| changeset 7228 | ddb67dcf026c |
| parent 7205 | dab2be236bfc |
| child 7257 | 745cfc8871e2 |
| 7227:a8e86b8e6fd1 | 7228:ddb67dcf026c |
|---|---|
5 |
5 |
6 Definitional introduction of datatypes |
6 Definitional introduction of datatypes |
7 Proof of characteristic theorems: |
7 Proof of characteristic theorems: |
8 |
8 |
9 - injectivity of constructors |
9 - injectivity of constructors |
10 - distinctness of constructors (internal version) |
10 - distinctness of constructors |
11 - induction theorem |
11 - induction theorem |
12 |
12 |
13 *) |
13 *) |
14 |
14 |
15 signature DATATYPE_REP_PROOFS = |
15 signature DATATYPE_REP_PROOFS = |