| 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
|