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