src/HOL/Set.thy
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"