src/HOL/Library/Multiset.thy

   order ["op \<le>#" "op <#"]
   by (auto intro: order.intro mset_le_refl mset_le_antisym
     mset_le_trans simp: mset_less_def)
 
 interpretation mset_order_cancel_semigroup:
-  pordered_cancel_ab_semigroup_add ["op \<le>#" "op <#" "op +"]
+  pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
   by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
 
 interpretation mset_order_semigroup_cancel:
-  pordered_ab_semigroup_add_imp_le ["op \<le>#" "op <#" "op +"]
+  pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
   by (unfold_locales) simp
 
 
 lemma mset_lessD:
   "\<lbrakk> A \<subset># B ; x \<in># A \<rbrakk> \<Longrightarrow> x \<in># B"