| changeset 25594 | 43c718438f9f |
| parent 25062 | af5ef0d4d655 |
| child 25691 | 8f8d83af100a |
| 25593:0b0df6c8646a | 25594:43c718438f9f |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Quotient types *} |
6 header {* Quotient types *} |
7 |
7 |
8 theory Quotient |
8 theory Quotient |
9 imports Main |
9 imports PreList Hilbert_Choice |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 We introduce the notion of quotient types over equivalence relations |
13 We introduce the notion of quotient types over equivalence relations |
14 via type classes. |
14 via type classes. |