| changeset 46026 | 83caa4f4bd56 |
| parent 45986 | c9e50153e5ae |
| child 46036 | 6a86cc88b02f |
--- a/src/HOL/Set.thy Wed Dec 28 22:08:44 2011 +0100 +++ b/src/HOL/Set.thy Thu Dec 29 10:47:54 2011 +0100 @@ -1804,7 +1804,7 @@ 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