equal
deleted
inserted
replaced
1 (* Title: quotient_def.thy |
1 (* Title: HOL/Tools/Quotient/quotient_def.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Definitions for constants on quotient types. |
4 Definitions for constants on quotient types. |
5 |
|
6 *) |
5 *) |
7 |
6 |
8 signature QUOTIENT_DEF = |
7 signature QUOTIENT_DEF = |
9 sig |
8 sig |
10 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |
9 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |