Brian Huffman wrote:
Attached is a mercurial changeset for adding mandatory qualifiers to
theorems generated by (rep_)datatype.
[...]
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.
I can take care of that, and also
On Tue, Nov 30, 2010 at 8:35 AM, Florian Haftmann
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 syst
>> 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 an
On Mon, Nov 29, 2010 at 11:47 PM, Florian Haftmann
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
