| Wed, 27 Oct 2010 11:10:36 -0700 |
huffman |
make domain package work with non-cpo argument types
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 14:19:59 -0700 |
huffman |
use Named_Thms instead of Theory_Data for some domain package theorems
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 10:13:29 -0700 |
huffman |
eliminate constant 'coerce'; use 'prj oo emb' instead
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 10:16:46 -0700 |
huffman |
add take_strict_thms field to take_info type
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 08:32:09 -0700 |
huffman |
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 18:46:19 -0700 |
huffman |
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
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
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 14:10:05 -0700 |
huffman |
separate map-related code into new function define_map_functions
|
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 12:21:07 -0800 |
huffman |
pass take_info as an argument to comp_theorems
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 11:58:40 -0800 |
huffman |
pass take_induct_info as an argument to comp_theorems
|
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
|
| Sun, 07 Mar 2010 13:34:53 -0800 |
huffman |
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 13:27:40 -0800 |
huffman |
fix proof script so qdomain_isomorphism foo = foo' works
|
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
|
| Tue, 02 Mar 2010 04:35:44 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 00:34:26 -0800 |
huffman |
domain package no longer generates copy functions; all proofs use take functions instead
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 16:58:16 -0800 |
huffman |
generate take_take rules
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 16:36:25 -0800 |
huffman |
add function define_take_functions
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 19:39:50 -0800 |
huffman |
domain_isomorphism package proves deflation rules for map functions
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 18:33:57 -0800 |
huffman |
store deflation thms for map functions in theory data
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 18:12:08 -0800 |
huffman |
use function list_ccomb
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 16:11:08 -0800 |
huffman |
add function define_const
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 15:30:44 -0800 |
huffman |
move common functions into new file holcf_library.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 15:09:09 -0800 |
huffman |
get rid of incomplete pattern match warnings
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 21:38:24 -0800 |
huffman |
domain_isomorphism function returns iso_info record
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2009 09:07:04 -0800 |
huffman |
add 'morphisms' option to domain_isomorphism command
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 12:17:43 +0100 |
haftmann |
modernized structure Datatype_Aux
|
file |
diff |
annotate
|
| Sun, 22 Nov 2009 22:04:51 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 22:25:11 -0800 |
huffman |
store map_ID thms in theory data; automate proofs of reach lemmas
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 21:06:22 -0800 |
huffman |
domain_isomorphism package defines combined copy function
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 17:53:22 -0800 |
huffman |
domain_isomorphism package defines copy functions
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 16:50:25 -0800 |
huffman |
copy_of_dtyp uses map table from theory data
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 15:31:19 -0800 |
huffman |
rename generated abs_iso, rep_iso lemmas
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 12:31:55 -0800 |
huffman |
automate proofs of map_ID theorems
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 12:05:49 -0800 |
huffman |
change Theory.requires
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 11:54:23 -0800 |
huffman |
use theory data for REP_simps and isodefl_rules
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 11:13:34 -0800 |
huffman |
replace defl_tab and map_tab with theory data
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 10:45:34 -0800 |
huffman |
separate conjuncts of isodefl theorem
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 10:27:29 -0800 |
huffman |
automate isodefl proof
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 09:04:58 -0800 |
huffman |
automate definition of map functions; remove unused code
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:22:00 -0800 |
huffman |
change naming convention for deflation combinators
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:00:42 -0800 |
huffman |
prove isomorphism and isodefl rules
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 16:14:28 -0800 |
huffman |
automate definition of rep/abs functions
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 15:54:47 -0800 |
huffman |
get rid of numbers on thy variables
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 15:51:35 -0800 |
huffman |
automate proofs of REP equations
|
file |
diff |
annotate
|