| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 13:27:35 -0700 |
huffman |
fix LaTeX overfull hbox warnings in HOLCF document
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 12:52:51 -0700 |
huffman |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 08:12:48 -0800 |
huffman |
move take-proofs stuff into new theory Domain_Aux.thy
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 14:05:25 -0800 |
huffman |
add comment
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 13:56:04 -0800 |
huffman |
move take_proofs-related stuff to a new section
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 10:40:40 -0800 |
huffman |
merged
|
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 16:43:55 +0100 |
wenzelm |
merged, resolving some basic conflicts;
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 18:16:28 -0800 |
huffman |
fixrec and repdef modules import holcf_library
|
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 13:50:23 -0800 |
huffman |
move take-related definitions and proofs to new module; simplify map_of_typ functions
|
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 15:30:44 -0800 |
huffman |
move common functions into new file holcf_library.ML
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 14:55:42 -0800 |
huffman |
move some powerdomain stuff into a new file
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:33:02 +0100 |
wenzelm |
cleanup type translations;
|
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 12:38:02 -0800 |
huffman |
set up domain_isomorphism package in Representable.thy
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 10:25:17 -0800 |
huffman |
add lemma isodefl_cprod
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:22:00 -0800 |
huffman |
change naming convention for deflation combinators
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 16:57:58 -0800 |
huffman |
remove one_typ and tr_typ; add abs/rep lemmas
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:31:20 -0800 |
huffman |
automate definition of representable domains from algebraic deflations
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 06:30:08 -0800 |
huffman |
add title/author block
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 06:22:29 -0800 |
huffman |
theory of representable cpos
|
file |
diff |
annotate
|