src/HOL/Library/Multiset.thy
changeset 49717 56494eedf493
parent 49394 52e636ace94e
child 49822 0cfc1651be25
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Oct 04 23:19:02 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Oct 04 23:19:02 2012 +0200
     1.3 @@ -872,6 +872,8 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +declare image_mset.identity [simp]
     1.8 +
     1.9  
    1.10  subsection {* Alternative representations *}
    1.11