changeset 922 | a2589b4bc442 |
parent 918 | 7be9b054f672 |
child 1097 | 551eacf071d7 |
--- a/Quot/Examples/AbsRepTest.thy Mon Jan 25 18:52:22 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Mon Jan 25 19:14:46 2010 +0100 @@ -2,8 +2,11 @@ imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List begin + +(* ML_command "ProofContext.debug := false" ML_command "ProofContext.verbose := false" +*) ML {* val ctxt0 = @{context}