multisets are partially ordered

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/MultisetOrder.thy	Mon May 22 12:35:02 2000 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/UNITY/MultisetOrder
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Multisets are partially ordered
+*)
+
+MultisetOrder = Multiset +
+
+instance multiset :: (order) order
+    (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le)
+
+end