# HG changeset patch
# User haftmann
# Date 1207575454 -7200
# Node ID 7bcebb8c2d33dca43e684a348e310f0dc2a870c9
# Parent  36a93808642cf59f869fcba3dcf22a59826a9c70
instantiation replacing primitive instance plus overloaded defs; more conservative type arities

diff -r 36a93808642c -r 7bcebb8c2d33 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Apr 07 15:37:33 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Apr 07 15:37:34 2008 +0200
@@ -712,11 +712,14 @@
 
 subsubsection {* Partial-order properties *}
 
-instance multiset :: (type) ord ..
+instantiation multiset :: (order) order
+begin
 
-defs (overloaded)
-  less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
-  le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
+definition
+  less_multiset_def: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition
+  le_multiset_def: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
 
 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
 unfolding trans_def by (blast intro: order_less_trans)
@@ -775,9 +778,7 @@
 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
 unfolding le_multiset_def by auto
 
-text {* Partial order. *}
-
-instance multiset :: (order) order
+instance
 apply intro_classes
    apply (rule mult_less_le)
   apply (rule mult_le_refl)
@@ -785,6 +786,8 @@
 apply (erule mult_le_antisym, assumption)
 done
 
+end
+
 
 subsubsection {* Monotonicity of multiset union *}