| Mon, 08 Mar 2010 12:36:26 -0800 |
huffman |
include take_info within take_induct_info type
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 11:48:29 -0800 |
huffman |
add type take_induct_info
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 11:34:53 -0800 |
huffman |
generate take_induct lemmas
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:37:03 -0800 |
huffman |
move proofs of reach and take lemmas to domain_take_proofs.ML
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 07:37:11 -0800 |
huffman |
add type take_info
|
file |
diff |
annotate
|
| 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
|