# HG changeset patch
# User Andreas Lochbihler
# Date 1338386721 -7200
# Node ID 918a92d4079f94b56e055687fe7fd464afdc857b
# Parent  d60f6b41bf2de934a2cd1e306a1b6bb1244030c1# Parent  4caf6cd063be74bd22884df0c8a7ffaf4615c707
merged

diff -r d60f6b41bf2d -r 918a92d4079f src/HOL/Library/Multiset.thy
--- 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