src/HOL/Library/Cset.thy
changeset 41505 6d19301074cf
parent 41372 551eb49a6e91
child 43241 93b1183e43e5
     1.1 --- a/src/HOL/Library/Cset.thy	Mon Jan 10 22:03:24 2011 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Tue Jan 11 14:12:37 2011 +0100
     1.3 @@ -188,7 +188,7 @@
     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: map
     1.8 +enriched_type map: map
     1.9    by (simp_all add: fun_eq_iff image_compose)
    1.10  
    1.11  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where