changeset 16417 | 9bc16273c2d4 |
parent 13615 | 449a70d88b38 |
child 24893 | b8ef7afe3a6b |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
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: |
10 theory QUniv imports Univ QPair begin |
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 |