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
|
Wed, 18 Nov 2009 15:01:00 -0800 |
huffman |
cleaned up; factored out fixed-point definition code
|
file |
diff |
annotate
|
Wed, 18 Nov 2009 12:41:43 -0800 |
huffman |
automate solution of domain equations
|
file |
diff |
annotate
|