# HG changeset patch
# User wenzelm
# Date 1434558149 -7200
# Node ID 47df24e05b1c9654d7b309043f5f659fbdf0c834
# Parent  c8141ac6f03f09ab80551034cf52fd26c758d387# Parent  aa58872267ee7d2d2193cb679779dd59c0e56196
merged

diff -r aa58872267ee -r 47df24e05b1c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jun 17 17:54:09 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 18:22:29 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 @@
 \<close>
 
 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 -