--- a/src/HOL/Library/Multiset.thy Wed Jun 17 17:33:22 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 17 18:13:44 2015 +0200
@@ -884,7 +884,7 @@
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
by simp
-lemma set_mset_image_mset [simp]:
+lemma set_image_mset [simp]:
"set_mset (image_mset f M) = image f (set_mset M)"
by (induct M) simp_all
@@ -928,7 +928,7 @@
*}
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
- by (metis mem_set_mset_iff set_mset_image_mset)
+by (metis mem_set_mset_iff set_image_mset)
functor image_mset: image_mset
proof -