| changeset 1129 | 9a86f0ef6503 |
| parent 1128 | 17ca92ab4660 |
| 1128:17ca92ab4660 | 1129:9a86f0ef6503 |
|---|---|
1 (* Title: Quotient_Product.thy |
1 (* Title: Quotient_Product.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 theory Quotient_Product |
4 theory Quotient_Product |
5 imports Quotient |
5 imports Quotient Quotient_Syntax |
6 begin |
6 begin |
7 |
7 |
8 section {* Quotient infrastructure for the product type. *} |
8 section {* Quotient infrastructure for the product type. *} |
9 |
9 |
10 fun |
10 fun |