equal
deleted
inserted
replaced
15 |
15 |
16 (* The class pcpo of pointed cpos *) |
16 (* The class pcpo of pointed cpos *) |
17 (* ****************************** *) |
17 (* ****************************** *) |
18 axclass pcpo < cpo |
18 axclass pcpo < cpo |
19 |
19 |
20 least "? x.!y.x<<y" |
20 least "? x.!y. x<<y" |
21 |
21 |
22 consts |
22 consts |
23 UU :: "'a::pcpo" |
23 UU :: "'a::pcpo" |
24 |
24 |
25 syntax (symbols) |
25 syntax (symbols) |
26 UU :: "'a::pcpo" ("\\<bottom>") |
26 UU :: "'a::pcpo" ("\\<bottom>") |
27 |
27 |
28 defs |
28 defs |
29 UU_def "UU == @x.!y.x<<y" |
29 UU_def "UU == @x.!y. x<<y" |
30 |
30 |
31 (* further useful classes for HOLCF domains *) |
31 (* further useful classes for HOLCF domains *) |
32 |
32 |
33 axclass chfin<cpo |
33 axclass chfin<cpo |
34 |
34 |
35 chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)" |
35 chfin "!Y. is_chain Y-->(? n. max_in_chain n Y)" |
36 |
36 |
37 axclass flat<pcpo |
37 axclass flat<pcpo |
38 |
38 |
39 ax_flat "! x y.x << y --> (x = UU) | (x=y)" |
39 ax_flat "! x y. x << y --> (x = UU) | (x=y)" |
40 |
40 |
41 end |
41 end |