Mon, 08 Mar 2010 11:58:40 -0800 | huffman | pass take_induct_info as an argument to comp_theorems | changeset | files |
Mon, 08 Mar 2010 11:48:29 -0800 | huffman | add type take_induct_info | changeset | files |
Mon, 08 Mar 2010 11:34:53 -0800 | huffman | generate take_induct lemmas | changeset | files |
Mon, 08 Mar 2010 09:37:03 -0800 | huffman | move proofs of reach and take lemmas to domain_take_proofs.ML | changeset | files |