[isabelle-dev] theorem "induct"
brianh at cs.pdx.edu
Tue Nov 30 15:42:40 CET 2010
On Mon, Nov 29, 2010 at 11:47 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> 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)
> 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.
Is there any reason why we shouldn't update the datatype package right
now, to make the qualifier mandatory on "foo.induct"?
More information about the isabelle-dev