| changeset 2278 | d63ffafce255 |
| parent 1479 | 21eb5e156d91 |
| child 2291 | fbd14a05fb88 |
| 2277:9174de6c7143 | 2278:d63ffafce255 |
|---|---|
12 cpo "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" |
12 cpo "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" |
13 |
13 |
14 inst_void_pcpo "(UU::void) = UU_void" |
14 inst_void_pcpo "(UU::void) = UU_void" |
15 |
15 |
16 (* start 8bit 1 *) |
16 (* start 8bit 1 *) |
17 syntax |
|
18 "GUU" :: "'a::pcpo" ("Ø") |
|
19 |
|
20 translations |
|
21 "Ø" == "UU" |
|
22 |
|
17 (* end 8bit 1 *) |
23 (* end 8bit 1 *) |
18 end |
24 end |