[isabelle-dev] theorem "induct"

[Sascha Boehme]

Hi,

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)
"induct".

Sascha