# HG changeset patch
# User wenzelm
# Date 966681911 -7200
# Node ID 80d14ea0e20057f655176b9e639cbe2cb7f3de02
# Parent  b9cf6801f3da7d1ae14167d6224f7b8743b65aef
turned into new-style theory;

diff -r b9cf6801f3da -r 80d14ea0e200 src/HOL/Induct/MultisetOrder.thy
--- a/src/HOL/Induct/MultisetOrder.thy	Sat Aug 19 12:44:39 2000 +0200
+++ b/src/HOL/Induct/MultisetOrder.thy	Sat Aug 19 12:45:11 2000 +0200
@@ -1,15 +1,28 @@
-(*  Title:      HOL/UNITY/MultisetOrder
+(*  Title:      HOL/Induct/MultisetOrder.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
-Multisets are partially ordered
+Multisets are partially ordered.
 *)
 
-MultisetOrder = Multiset +
+theory MultisetOrder = Multiset:
 
 instance multiset :: (order) order
-    (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le)
+  apply intro_classes
+     apply (rule mult_le_refl)
+    apply (erule mult_le_trans)
+    apply assumption
+   apply (erule mult_le_antisym)
+   apply assumption
+  apply (rule mult_less_le)
+  done
 
-instance multiset :: (term) plus_ac0 (union_commute,union_assoc) {|Auto_tac|}
+instance multiset :: ("term") plus_ac0
+  apply intro_classes
+    apply (rule union_commute)
+   apply (rule union_assoc)
+  apply simp
+  done
+
 end