[isabelle-dev] theorem "induct"

[Brian Huffman]

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