equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 defaultsort type |
12 defaultsort type |
13 |
13 |
14 pcpodef 'a lift = "UNIV :: 'a discr u set" |
14 pcpodef 'a lift = "UNIV :: 'a discr u set" |
15 by simp |
15 by simp_all |
16 |
16 |
17 instance lift :: (finite) finite_po |
17 instance lift :: (finite) finite_po |
18 by (rule typedef_finite_po [OF type_definition_lift]) |
18 by (rule typedef_finite_po [OF type_definition_lift]) |
19 |
19 |
20 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |
20 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |