src/HOL/Library/Cset.thy
changeset 41372 551eb49a6e91
parent 40968 a6fcd305f7dc
child 41505 6d19301074cf
     1.1 --- a/src/HOL/Library/Cset.thy	Tue Dec 21 16:14:46 2010 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Tue Dec 21 17:52:23 2010 +0100
     1.3 @@ -188,8 +188,8 @@
     1.4    "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
     1.5    by (simp add: set_def)
     1.6  
     1.7 -type_lifting map
     1.8 -  by (simp_all add: image_image)
     1.9 +type_lifting map: map
    1.10 +  by (simp_all add: fun_eq_iff image_compose)
    1.11  
    1.12  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.13    [simp]: "filter P A = Set (More_Set.project P (member A))"