Dear HOL4 experts,
Isabelle documentation ("Programming and Proving in Isabelle/HOL",
section 4.4.6) shows how one can apply "advanced rule induction" to
goals where an argument of some inductive predicate is not a variable,
for example,
"EVEN (SUC n) ==> ~ EVEN n".
I could not find anything similar in HOL4 -- did I missed something?
--
Regards,
Piotr Trojanek
------------------------------------------------------------------------------
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
