# HG changeset patch
# User haftmann
# Date 1290096075 -3600
# Node ID c0770657c8dec6d08c1be6a0f0717b5c0d45ad5b
# Parent  963ee2331d20fd7be1ab2b3ca13577abd3152fff
mapper for fset type

diff -r 963ee2331d20 -r c0770657c8de src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Thu Nov 18 17:01:15 2010 +0100
+++ b/src/HOL/Library/Fset.thy	Thu Nov 18 17:01:15 2010 +0100
@@ -178,6 +178,9 @@
   "map f (Set xs) = Set (remdups (List.map f xs))"
   by (simp add: Set_def)
 
+type_mapper map
+  by (simp_all add: image_image)
+
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   [simp]: "filter P A = Fset (More_Set.project P (member A))"