src/HOL/Library/Multiset.thy

 apply (subst elem_imp_eq_diff_union[symmetric])
  apply (simp add: nth_mem_multiset_of)
 apply simp
 done
 
-interpretation mset_order!: order "op \<le>#" "op <#"
+interpretation mset_order: order "op \<le>#" "op <#"
 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
   mset_le_trans simp: mset_less_def)
 
-interpretation mset_order_cancel_semigroup!:
+interpretation mset_order_cancel_semigroup:
   pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
 proof qed (erule mset_le_mono_add [OF mset_le_refl])
 
-interpretation mset_order_semigroup_cancel!:
+interpretation mset_order_semigroup_cancel:
   pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
 proof qed simp
 
 
 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"

 subsection {* Image *}
 
 definition [code del]:
  "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_left_comm!: left_commutative "op + o single o f"
+interpretation image_left_comm: left_commutative "op + o single o f"
   proof qed (simp add:union_ac)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)