equal
deleted
inserted
replaced
1 Pcpo = Porder + |
1 Pcpo = Porder + |
2 |
2 |
3 classes pcpo < po |
3 classes pcpo < po |
|
4 |
4 arities void :: pcpo |
5 arities void :: pcpo |
5 |
6 |
6 consts |
7 consts |
7 UU :: "'a::pcpo" |
8 |
|
9 UU :: "'a::pcpo" |
|
10 |
|
11 syntax (symbols) |
|
12 |
|
13 UU :: "'a::pcpo" ("\\<bottom>") |
8 |
14 |
9 rules |
15 rules |
10 |
16 |
11 minimal "UU << x" |
17 minimal "UU << x" |
12 cpo "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" |
18 cpo "is_chain S ==> ? x. range(S) <<| (x::'a::pcpo)" |
13 |
19 |
14 inst_void_pcpo "(UU::void) = UU_void" |
20 inst_void_pcpo "(UU::void) = UU_void" |
15 |
21 |
16 (* start 8bit 1 *) |
|
17 (* end 8bit 1 *) |
|
18 end |
22 end |