--- a/src/HOL/Isar_examples/ROOT.ML Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/Isar_examples/ROOT.ML Thu Nov 08 23:50:08 2001 +0100
@@ -13,7 +13,9 @@
time_use_thy "Summation";
time_use_thy "KnasterTarski";
time_use_thy "MutilatedCheckerboard";
-with_path "../W0" time_use_thy "W_correct";
+with_path "../W0" (no_document time_use_thy) "Type";
+with_path "../W0" time_use_thy "W_correct";
+with_path "../NumberTheory" (no_document time_use_thy) "Primes";
with_path "../NumberTheory" time_use_thy "Fibonacci";
time_use_thy "Puzzle";
time_use_thy "NestedDatatype";