Wed, 03 Mar 2010 08:20:20 -0800 | huffman | remove unnecessary theorem references | changeset | files |
Wed, 03 Mar 2010 08:14:56 -0800 | huffman | remove copy_of_dtyp from domain_axioms.ML | changeset | files |
Wed, 03 Mar 2010 07:55:52 -0800 | huffman | add_axioms returns an iso_info; add_theorems takes an iso_info as an argument | changeset | files |
Wed, 03 Mar 2010 07:36:31 -0800 | huffman | uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate | changeset | files |
Wed, 03 Mar 2010 06:48:00 -0800 | huffman | add function axiomatize_lub_take | changeset | files |
Wed, 03 Mar 2010 06:25:42 -0800 | huffman | move function mk_lub into holcf_library.ML | changeset | files |