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