equal
deleted
inserted
replaced
1 (* Title: quotient_typ.thy |
1 (* Title: HOL/Tools/Quotient/quotient_typ.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Definition of a quotient type. |
4 Definition of a quotient type. |
5 |
|
6 *) |
5 *) |
7 |
6 |
8 signature QUOTIENT_TYPE = |
7 signature QUOTIENT_TYPE = |
9 sig |
8 sig |
10 val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm |
9 val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm |