# HG changeset patch
# User wenzelm
# Date 971904956 -7200
# Node ID 21055ac277083af0aaf44abae511d4311e1374f9
# Parent  320a4084dfac2636c926353b7c72cf80af88ea3b
MultisetOrder mmoved to HOL/Library;

diff -r 320a4084dfac -r 21055ac27708 src/HOL/Isar_examples/ROOT.ML
--- 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";
diff -r 320a4084dfac -r 21055ac27708 src/HOL/Isar_examples/document/root.tex
--- 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}