On Thu, 12 Mar 2015, Michael Norrish wrote:
I’ve made a feature request on Github
(https://github.com/HOL-Theorem-Prover/HOL/issues/244), which may help
remind me to implement this very nice feature. (Not that it *has* to be
me that implements it…)
Funny. Note that the Isabelle situation is a bit convoluted after many
years of advanced "induct", "induction", "coinduct", "coinduction". A bit
too many authors have worked on cumulatively "better" versions, but there
is nobody who understands all details.
Of course, it *has* to be me to clear it out one day, unless some
unexpected miracle happens.
Makarius------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
