Fri, 26 Feb 2010 09:10:50 -0800 | huffman | move constructor-specific stuff to a separate function | changeset | files |
Fri, 26 Feb 2010 08:49:59 -0800 | huffman | replace prove_thm function | changeset | files |
Fri, 26 Feb 2010 08:37:03 -0800 | huffman | move proof of compactness rules into domain_constructors.ML | changeset | files |