| changeset 952 | 9c3b3eaecaff |
| parent 918 | 7be9b054f672 |
| child 1101 | 5eb84b817855 |
| 951:62f0344b219c | 952:9c3b3eaecaff |
|---|---|
1 (* Title: quotient_typ.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Definition of a quotient type. |
|
5 |
|
6 *) |
|
7 |
|
1 signature QUOTIENT_TYPE = |
8 signature QUOTIENT_TYPE = |
2 sig |
9 sig |
3 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
10 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
4 -> Proof.context -> Proof.state |
11 -> Proof.context -> Proof.state |
5 |
12 |