[isabelle-dev] theorem "induct"

Sascha Boehme boehmes at in.tum.de
Tue Nov 30 08:39:40 CET 2010


There exists a theorem called "induct" in HOL, which changes after
every datatype declaration.  What is the rationale behind this
theorem?  Is it required for a particular purpose or just a forgotten
remainder of previous tunings?  Shouldn't this suprising behaviour be
eliminated?  Note that each datatype declaration "foo" also introduces
a theorem "foo.induct" which looks identical to (the most recent)


More information about the isabelle-dev mailing list