| Mon, 08 Mar 2010 07:22:30 -0800 | huffman | add function add_qualified_def | file | diff | annotate |
| Fri, 05 Mar 2010 13:55:36 -0800 | huffman | remove dead code | file | diff | annotate |
| Thu, 04 Mar 2010 08:12:39 -0800 | huffman | add function add_qualified_simp_thm | file | diff | annotate |
| Wed, 03 Mar 2010 21:42:42 -0800 | huffman | generate lemma take_below, declare chain_take [simp] | file | diff | annotate |
| 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 | file | diff | annotate |
| Wed, 03 Mar 2010 06:25:42 -0800 | huffman | move function mk_lub into holcf_library.ML | file | diff | annotate |
| Tue, 02 Mar 2010 14:33:34 -0800 | huffman | move definition of finiteness predicate into domain_take_proofs.ML | file | diff | annotate |
| Tue, 02 Mar 2010 13:50:23 -0800 | huffman | move take-related definitions and proofs to new module; simplify map_of_typ functions | file | diff | annotate |