Sat, 27 Feb 2010 15:32:42 -0800 | huffman | move definition of discriminators to domain_constructors.ML | changeset | files |
Sat, 27 Feb 2010 14:04:46 -0800 | huffman | move proofs of when_rews intro domain_constructors.ML | changeset | files |
Sat, 27 Feb 2010 10:12:47 -0800 | huffman | moved proofs of dist_les and dist_eqs to domain_constructors.ML | changeset | files |
Sat, 27 Feb 2010 08:30:11 -0800 | huffman | move proofs of casedist into domain_constructors.ML | changeset | files |
Fri, 26 Feb 2010 10:54:52 -0800 | huffman | move proofs of injects and inverts to domain_constructors.ML | changeset | files |
Fri, 26 Feb 2010 10:11:37 -0800 | huffman | reuse vars_of function | changeset | files |