
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}




