--- a/src/HOL/Library/Multiset.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Mar 26 20:08:55 2009 +0100
@@ -1077,15 +1077,15 @@
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
@@ -1433,7 +1433,7 @@
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 {#} = {#}"