changeset 1128 | 17ca92ab4660 |
parent 944 | 6267ad688ea8 |
child 1137 | 36d596cb63a2 |
child 1139 | c4001cda9da3 |
1127:243a5ceaa088 | 1128:17ca92ab4660 |
---|---|
1 theory FSet |
1 theory FSet |
2 imports "../QuotMain" "../QuotList" "../QuotProd" List |
2 imports "../Quotient" "../Quotient_List" "../Quotient_Product" List |
3 begin |
3 begin |
4 |
4 |
5 inductive |
5 inductive |
6 list_eq (infix "\<approx>" 50) |
6 list_eq (infix "\<approx>" 50) |
7 where |
7 where |