equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Quotient.thy |
1 (* Title: HOL/Library/Quotient.thy |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Quotient types *} |
5 header {* Quotient types *} |
7 |
6 |
8 theory Quotient |
7 theory Quotient |
9 imports Plain "~~/src/HOL/Hilbert_Choice" |
8 imports Main |
10 begin |
9 begin |
11 |
10 |
12 text {* |
11 text {* |
13 We introduce the notion of quotient types over equivalence relations |
12 We introduce the notion of quotient types over equivalence relations |
14 via type classes. |
13 via type classes. |