--- a/src/HOL/Library/Multiset.thy Thu Oct 04 23:19:02 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Oct 04 23:19:02 2012 +0200 @@ -872,6 +872,8 @@ qed qed +declare image_mset.identity [simp] + subsection {* Alternative representations *}