diff -r dae038c8cd69 -r a2589b4bc442 Quot/Examples/AbsRepTest.thy --- 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}