src/HOL/Library/Multiset.thy
changeset 49717 56494eedf493
parent 49394 52e636ace94e
child 49822 0cfc1651be25
--- 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 *}