src/HOL/Isar_examples/ROOT.ML

--- a/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:24:56 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:25:19 1999 +0200
@@ -10,9 +10,7 @@
 time_use_thy "Cantor";
 time_use_thy "ExprCompiler";
 time_use_thy "Group";
-time_use_thy "NatSum";
+time_use_thy "Summation";
 time_use_thy "KnasterTarski";
 time_use_thy "MutilatedCheckerboard";
-
-add_path "../Induct";
-time_use_thy "MultisetOrder";
+with_path "../Induct" time_use_thy "MultisetOrder";