# HG changeset patch
# User wenzelm
# Date 936215161 -7200
# Node ID 1f8ce3f7ccb4866e2e0517bf7e38e3ecf3cc5c78
# Parent  878693c6855679587b7cc4d6bcd7c88fbd2896fc
added MultisetOrder.thy;

diff -r 878693c68556 -r 1f8ce3f7ccb4 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Wed Sep 01 21:45:48 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Wed Sep 01 21:46:01 1999 +0200
@@ -13,3 +13,6 @@
 time_use_thy "NatSum";
 time_use_thy "KnasterTarski";
 time_use_thy "MutilatedCheckerboard";
+
+add_path "../Induct";
+time_use_thy "MultisetOrder";