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