| 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 |
| Fri, 15 Oct 2010 05:50:27 -0700 | huffman | rewrite proof automation for finite_ind; get rid of case_UU_tac | changeset | files |
| Thu, 14 Oct 2010 19:16:52 -0700 | huffman | put constructor argument specs in constr_info type | changeset | files |
| Thu, 14 Oct 2010 14:42:05 -0700 | huffman | avoid using Global_Theory.get_thm | changeset | files |
| Thu, 14 Oct 2010 13:46:27 -0700 | huffman | include iso_info as part of constr_info type | changeset | files |
| Thu, 14 Oct 2010 13:28:31 -0700 | huffman | remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors | changeset | files |