Hi Sascha, > 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".
indeed, both theorems are the same, just with different accesses;
recently, we introduced the concept of mandatory qualifiers to avoid the
strange base accesses (e.g. »induct«, »simps«, »intros«), but this has
never been systematically introduces into existing packages.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
