| Sat, 16 Oct 2010 16:39:06 -0700 | huffman | merged | changeset | files |
| Sat, 16 Oct 2010 16:22:42 -0700 | huffman | remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check | changeset | files |
| Sat, 16 Oct 2010 15:26:30 -0700 | huffman | reimplement proof automation for coinduct rules | changeset | files |
| Sat, 16 Oct 2010 14:41:11 -0700 | huffman | add functions mk_imp, mk_all | changeset | files |
| Fri, 15 Oct 2010 08:52:53 -0700 | huffman | move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code | changeset | files |
| Fri, 15 Oct 2010 08:07:20 -0700 | huffman | simplify automation of induct proof | changeset | files |
| Fri, 15 Oct 2010 06:08:42 -0700 | huffman | add function mk_adm | changeset | files |