src/HOL/Set.thy
changeset 46026 83caa4f4bd56
parent 45986 c9e50153e5ae
child 46036 6a86cc88b02f
     1.1 --- a/src/HOL/Set.thy	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -1804,7 +1804,7 @@
     1.4  hide_const (open) remove
     1.5  
     1.6  definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     1.7 -  "project P A = {a \<in> A. P a}"
     1.8 +  [code_abbrev]: "project P A = {a \<in> A. P a}"
     1.9  
    1.10  hide_const (open) project
    1.11