changeset 15577 | e16da3068ad6 |
parent 15576 | efb95d0d01f7 |
child 15651 | 4b393520846e |
15576:efb95d0d01f7 | 15577:e16da3068ad6 |
---|---|
3 Author: Olaf Mueller |
3 Author: Olaf Mueller |
4 *) |
4 *) |
5 |
5 |
6 header {* Lifting types of class type to flat pcpo's *} |
6 header {* Lifting types of class type to flat pcpo's *} |
7 |
7 |
8 theory Lift = Cprod: |
8 theory Lift |
9 imports Cprod |
|
10 begin |
|
9 |
11 |
10 defaultsort type |
12 defaultsort type |
11 |
13 |
12 |
14 |
13 typedef 'a lift = "UNIV :: 'a option set" .. |
15 typedef 'a lift = "UNIV :: 'a option set" .. |