[isabelle-dev] theorem "induct"

[Brian Huffman]

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

induct
inject
distinct
exhaust
cases
split
split_asm
weak_case_cong
nchotomy
case_cong

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.

- Brian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: qualified.diff
Type: text/x-patch
Size: 4388 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101130/bc7a3f46/attachment-0002.bin>