changeset 1128 | 17ca92ab4660 |
parent 1097 | 551eacf071d7 |
child 1150 | 689a18f9484c |
1127:243a5ceaa088 | 1128:17ca92ab4660 |
---|---|
1 theory AbsRepTest |
1 theory AbsRepTest |
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
2 imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 (* |
6 (* |
7 ML_command "ProofContext.debug := false" |
7 ML_command "ProofContext.debug := false" |