| changeset 13357 | 6f54e992777e |
| parent 13356 | c9cfe1638bf2 |
| child 13615 | 449a70d88b38 |
| 13356:c9cfe1638bf2 | 13357:6f54e992777e |
|---|---|
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*A Small Universe for Lazy Recursive Types*} |
8 header{*A Small Universe for Lazy Recursive Types*} |
9 |
9 |
10 theory QUniv = Univ + QPair + mono + equalities: |
10 theory QUniv = Univ + QPair: |
11 |
11 |
12 (*Disjoint sums as a datatype*) |
12 (*Disjoint sums as a datatype*) |
13 rep_datatype |
13 rep_datatype |
14 elimination sumE |
14 elimination sumE |
15 induction TrueI |
15 induction TrueI |