merged

--- a/src/HOL/Library/Multiset.thy	Wed May 30 16:05:06 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed May 30 16:05:21 2012 +0200
@@ -827,6 +827,9 @@
 apply (simp add: add_assoc [symmetric] image_mset_insert)
 done
 
+lemma set_of_image_mset [simp]: "set_of (image_mset f M) = image f (set_of M)"
+by (induct M) simp_all
+
 lemma size_image_mset [simp]: "size (image_mset f M) = size M"
 by (induct M) simp_all