| changeset 42163 | 392fd6c4669c |
| parent 41107 | 8795cd75965e |
| child 42284 | 326f57825e1a |
--- a/src/HOL/Set.thy Wed Mar 30 11:32:51 2011 +0200 +++ b/src/HOL/Set.thy Wed Mar 30 11:32:52 2011 +0200 @@ -8,7 +8,7 @@ subsection {* Sets as predicates *} -types 'a set = "'a \<Rightarrow> bool" +type_synonym 'a set = "'a \<Rightarrow> bool" definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension" "Collect P = P"