Tue, 02 Mar 2010 14:35:09 -0800 | huffman | get rid of primes on thy variables | changeset | files |
Tue, 02 Mar 2010 14:33:34 -0800 | huffman | move definition of finiteness predicate into domain_take_proofs.ML | changeset | files |
Tue, 02 Mar 2010 13:50:23 -0800 | huffman | move take-related definitions and proofs to new module; simplify map_of_typ functions | changeset | files |