[isabelle-dev] theorem "induct"
brianh at cs.pdx.edu
Tue Nov 30 20:11:32 CET 2010
On Tue, Nov 30, 2010 at 8:35 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
>>> 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"?
> Maybe this is a good opportunity. Maybe this should be done to every
> package which has no specific maintainer.
Attached is a mercurial changeset for adding mandatory qualifiers to
theorems generated by (rep_)datatype. Here are the affected theorem
names (that I know of):
I've only tested this with HOL-Main; I'll let someone else test it
more thoroughly and decide whether or not to commit it.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 4388 bytes
Desc: not available
More information about the isabelle-dev