--- a/src/HOL/Isar_examples/ROOT.ML Wed Oct 18 23:35:08 2000 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML Wed Oct 18 23:35:56 2000 +0200
@@ -13,7 +13,6 @@
time_use_thy "Summation";
time_use_thy "KnasterTarski";
time_use_thy "MutilatedCheckerboard";
-with_path "../Induct" time_use_thy "MultisetOrder";
with_path "../W0" time_use_thy "W_correct";
with_path "../NumberTheory" time_use_thy "Fibonacci";
time_use_thy "Puzzle";
--- a/src/HOL/Isar_examples/document/root.tex Wed Oct 18 23:35:08 2000 +0200
+++ b/src/HOL/Isar_examples/document/root.tex Wed Oct 18 23:35:56 2000 +0200
@@ -31,10 +31,6 @@
\input{Summation.tex}
\input{KnasterTarski.tex}
\input{MutilatedCheckerboard.tex}
-%\input{Multiset0.tex}
-%\input{Acc.tex}
-%\input{Multiset.tex}
-\input{MultisetOrder.tex}
%\input{Maybe.tex}
%\input{Type.tex}
\input{W_correct.tex}