# HG changeset patch
# User paulson
# Date 958991702 -7200
# Node ID 433843c1b454dcd5d7b7bf3ca9adedb65b215607
# Parent  80303d9b0d7b921d28183f9e20e626933c39c5cc
multisets are partially ordered

diff -r 80303d9b0d7b -r 433843c1b454 src/HOL/Induct/MultisetOrder.thy
--- /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