| 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
|
| Wed, 03 Mar 2010 07:55:52 -0800 |
huffman |
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 20:04:17 -0800 |
huffman |
simplify add_axioms function; remove obsolete domain_syntax.ML
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:21:10 -0800 |
huffman |
proper names for types cfun, sprod, ssum
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:53:07 -0800 |
huffman |
remove unused mixfix component from type cons
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:46:23 -0800 |
huffman |
cleaned up, added type annotations
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:06:02 -0800 |
huffman |
remove unused selector field from type arg
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 14:59:24 -0800 |
huffman |
add_syntax no longer needs a definitional mode
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 14:41:16 -0800 |
huffman |
add_axioms no longer needs a definitional mode
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 14:35:09 -0800 |
huffman |
get rid of primes on thy variables
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 04:35:44 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 04:31:50 -0800 |
huffman |
re-enable bisim code, now in domain_theorems.ML
|
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
|
| Sat, 27 Feb 2010 21:38:24 -0800 |
huffman |
domain_isomorphism function returns iso_info record
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 16:15:03 -0800 |
huffman |
reorganizing domain package code (in progress)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:20:07 -0800 |
huffman |
change domain package's treatment of variable names in theorems to be like datatype package
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 11:17:41 -0800 |
huffman |
add mixfix field to type Domain_Library.cons
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
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
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 15:41:52 -0800 |
huffman |
clean up indentation; add 'definitional' option flag
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 13:23:58 -0800 |
huffman |
clean up indentation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 16:14:56 +0200 |
haftmann |
obey captialized directory names convention
|
file |
diff |
annotate
| base
|