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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
