# HG changeset patch # User haftmann # Date 1349385542 -7200 # Node ID 56494eedf4933c5de394d1b6ab0d62dd3e7b2705 # Parent c55b39740529bd3f2dfe30cb0ae1cc4cf958b4e3 default simp rule for image under identity diff -r c55b39740529 -r 56494eedf493 src/HOL/Library/Multiset.thy --- 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 *}