Wed, 20 Oct 2010 16:19:25 -0700 | huffman | combine check_and_sort_domain with main function; rewrite much of the error-checking code | changeset | files |
Wed, 20 Oct 2010 13:22:30 -0700 | huffman | constructor arguments with selectors must have pointed types | changeset | files |
Wed, 20 Oct 2010 13:02:13 -0700 | huffman | simplify check_and_sort_domain; more meaningful variable names | changeset | files |
Tue, 19 Oct 2010 16:21:24 -0700 | huffman | replace fixrec 'permissive' mode with per-equation 'unchecked' option | changeset | files |
Tue, 19 Oct 2010 15:01:51 -0700 | huffman | rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML | changeset | files |
Tue, 19 Oct 2010 14:28:14 -0700 | huffman | simplify some proofs; remove some unused lists of lemmas | changeset | files |