# HG changeset patch
# User paulson
# Date 958991314 -7200
# Node ID e9c34ab7d604e9c047c2b0c6768e4c7f9f91dfa2
# Parent  c35b74bad518a8cbc7d0f0bf872346945553966b
new file Induct/MultisetOrder.thy

diff -r c35b74bad518 -r e9c34ab7d604 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 22 12:27:11 2000 +0200
+++ b/src/HOL/IsaMakefile	Mon May 22 12:28:34 2000 +0200
@@ -134,8 +134,9 @@
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
-  Induct/Multiset0.ML Induct/Multiset0.thy Induct/Multiset.ML \
-  Induct/Multiset.thy Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
+  Induct/Multiset0.ML Induct/Multiset0.thy \
+  Induct/Multiset.ML Induct/Multiset.thy Induct/MultisetOrder.thy \
+  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
   Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
   Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
   Induct/Term.ML Induct/Term.thy