src/HOL/Infinite_Set.thy

--- a/src/HOL/Infinite_Set.thy	Tue Mar 21 15:38:53 2006 +0100
+++ b/src/HOL/Infinite_Set.thy	Wed Mar 22 11:14:58 2006 +0100
@@ -13,10 +13,8 @@
 
 text {* Some elementary facts about infinite sets, by Stefan Merz. *}
 
-syntax
-  infinite :: "'a set \<Rightarrow> bool"
-translations
-  "infinite S" == "S \<notin> Finites"
+abbreviation (output)
+  "infinite S = (S \<notin> Finites)"
 
 text {*
   Infinite sets are non-empty, and if we remove some elements