changeset 15576 | efb95d0d01f7 |
parent 14981 | e73f8140af78 |
child 15577 | e16da3068ad6 |
15575:63babb1ee883 | 15576:efb95d0d01f7 |
---|---|
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 = Cprod3: |
8 theory Lift = Cprod: |
9 |
9 |
10 defaultsort type |
10 defaultsort type |
11 |
11 |
12 |
12 |
13 typedef 'a lift = "UNIV :: 'a option set" .. |
13 typedef 'a lift = "UNIV :: 'a option set" .. |