src/HOL/Set.thy

   "remove x A = A - {x}"
 
 hide_const (open) remove
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a \<in> A. P a}"
+  [code_abbrev]: "project P A = {a \<in> A. P a}"
 
 hide_const (open) project
 
 instantiation set :: (equal) equal
 begin