| changeset 47455 | 26315a545e26 |
| parent 47308 | 9caab698dbe4 |
| child 47624 | 16d433895d2e |
| 47454:479b4d6b9562 | 47455:26315a545e26 |
|---|---|
1 (* Title: HOL/Library/Quotient3_Option.thy |
1 (* Title: HOL/Library/Quotient_Option.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 option type *} |
5 header {* Quotient infrastructure for the option type *} |
6 |
6 |