--- a/src/HOL/ex/ROOT.ML Thu Oct 11 21:10:43 2007 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Oct 11 21:44:28 2007 +0200
@@ -83,7 +83,9 @@
time_use_thy "Sudoku"
else ();
+(*
time_use_thy "Refute_Examples";
+*)
time_use_thy "Quickcheck_Examples";
no_document time_use_thy "NormalForm";