mapper for fset type
authorhaftmann
Thu, 18 Nov 2010 17:01:15 +0100
changeset 40604 c0770657c8de
parent 40603 963ee2331d20
child 40605 0bc28f978bcf
mapper for fset type
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))"