On Mon, Nov 29, 2010 at 11:47 PM, Florian Haftmann <[email protected]> wrote: > 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
Is there any reason why we shouldn't update the datatype package right now, to make the qualifier mandatory on "foo.induct"? - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
