[isabelle-dev] theorem "induct"

Alexander Krauss krauss at in.tum.de
Tue Nov 30 22:18:55 CET 2010

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 look at other packages while we are at it.


More information about the isabelle-dev mailing list