equal
deleted
inserted
replaced
13 |
13 |
14 defaultsort cpo |
14 defaultsort cpo |
15 |
15 |
16 subsection {* Type @{typ unit} is a pcpo *} |
16 subsection {* Type @{typ unit} is a pcpo *} |
17 |
17 |
18 instantiation unit :: sq_ord |
18 instantiation unit :: po |
19 begin |
19 begin |
20 |
20 |
21 definition |
21 definition |
22 less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True" |
22 less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True" |
23 |
23 |
24 instance .. |
24 instance |
|
25 by intro_classes simp_all |
|
26 |
25 end |
27 end |
26 |
|
27 instance unit :: po |
|
28 by intro_classes simp_all |
|
29 |
28 |
30 instance unit :: finite_po .. |
29 instance unit :: finite_po .. |
31 |
30 |
32 instance unit :: pcpo |
31 instance unit :: pcpo |
33 by intro_classes simp |
32 by intro_classes simp |