| changeset 49759 | ecf1d5d87e5e |
| parent 42814 | 5af15f1e2ef6 |
| child 51717 | 9e7d1c139569 |
| 49758:718f10c8bbfc | 49759:ecf1d5d87e5e |
|---|---|
8 imports Discrete Up |
8 imports Discrete Up |
9 begin |
9 begin |
10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 pcpodef (open) 'a lift = "UNIV :: 'a discr u set" |
13 pcpodef 'a lift = "UNIV :: 'a discr u set" |
14 by simp_all |
14 by simp_all |
15 |
15 |
16 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |
16 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |
17 |
17 |
18 definition |
18 definition |