changeset 36452 | d37c6eed8117 |
parent 35948 | 5e7909f0346b |
child 37099 | 3636b08cbf51 |
36451:ddc965e172c4 | 36452:d37c6eed8117 |
---|---|
6 |
6 |
7 theory Lift |
7 theory Lift |
8 imports Discrete Up Countable |
8 imports Discrete Up Countable |
9 begin |
9 begin |
10 |
10 |
11 defaultsort type |
11 default_sort type |
12 |
12 |
13 pcpodef '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 instance lift :: (finite) finite_po |
16 instance lift :: (finite) finite_po |