| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Fri, 28 May 2010 18:15:22 +0200 |
wenzelm |
made SML/NJ quite happy;
|
file |
diff |
annotate
|
| Sat, 22 May 2010 08:30:40 -0700 |
huffman |
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 13:44:28 -0700 |
huffman |
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:30:38 -0800 |
huffman |
more consistent use of qualified bindings
|
file |
diff |
annotate
|
| 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
|