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 |
Mon, 08 Mar 2010 09:33:05 -0800 | huffman | move lemmas from Domain.thy to Domain_Aux.thy | changeset | files |