# HG changeset patch
# User haftmann
# Date 1290096076 -3600
# Node ID af1a0b0c6202f7c1c6e77dae01be8e0967b3a2c5
# Parent  0bc28f978bcfcdb43c6c2b4e3f23e6d1c65eb919
mapper for mulitset type

diff -r 0bc28f978bcf -r af1a0b0c6202 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 18 17:01:16 2010 +0100
@@ -1627,6 +1627,14 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
+type_mapper image_mset proof -
+  fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
+    by (induct A) simp_all
+next
+  fix A show "image_mset (\<lambda>x. x) A = A"
+    by (induct A) simp_all
+qed
+
 
 subsection {* Termination proofs with multiset orders *}