changeset 1128 | 17ca92ab4660 |
parent 856 | 433f7c17255f |
child 1139 | c4001cda9da3 |
1127:243a5ceaa088 | 1128:17ca92ab4660 |
---|---|
1 theory FSet3 |
1 theory FSet3 |
2 imports "../QuotMain" "../QuotList" List |
2 imports "../Quotient" "../Quotient_List" List |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 structure QuotientRules = Named_Thms |
6 structure QuotientRules = Named_Thms |
7 (val name = "quot_thm" |
7 (val name = "quot_thm" |