| Sun, 19 Dec 2010 06:59:01 -0800 |
huffman |
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 06:39:19 -0800 |
huffman |
powerdomain theories require class 'bifinite' instead of 'domain'
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 06:34:41 -0800 |
huffman |
type 'defl' takes a type parameter again (cf. b525988432e9)
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 05:15:31 -0800 |
huffman |
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 16:43:45 -0800 |
huffman |
renamed CompactBasis.thy to Compact_Basis.thy
|
file |
diff |
annotate
|
| Sat, 11 Dec 2010 11:26:37 -0800 |
huffman |
xsymbol notation for powerdomain types
|
file |
diff |
annotate
|
| Sat, 11 Dec 2010 10:35:40 -0800 |
huffman |
new powerdomain lemmas
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 14:17:35 -0800 |
huffman |
add set-union-like syntax for powerdomain bind operators
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:29:39 -0800 |
huffman |
reformulate lemma preorder.ex_ideal, and use it for typedefs
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 16:08:10 -0800 |
huffman |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file |
diff |
annotate
| base
|