| changeset 952 | 9c3b3eaecaff |
| parent 884 | e49c6b6f37f4 |
| child 1097 | 551eacf071d7 |
| 951:62f0344b219c | 952:9c3b3eaecaff |
|---|---|
1 (* Title: quotient_def.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Definitions for constants on quotient types. |
|
5 |
|
6 *) |
|
1 |
7 |
2 signature QUOTIENT_DEF = |
8 signature QUOTIENT_DEF = |
3 sig |
9 sig |
4 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
10 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
5 local_theory -> (term * thm) * local_theory |
11 local_theory -> (term * thm) * local_theory |