| changeset 47455 | 26315a545e26 |
| parent 47308 | 9caab698dbe4 |
| child 47626 | f7b1034cb9ce |
| 47454:479b4d6b9562 | 47455:26315a545e26 |
|---|---|
1 (* Title: HOL/Library/Quotient3_Set.thy |
1 (* Title: HOL/Library/Quotient_Set.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 header {* Quotient infrastructure for the set type *} |
5 header {* Quotient infrastructure for the set type *} |
6 |
6 |