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. Alex _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
