src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 29 17:53:43 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