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