src/HOL/Infinite_Set.thy

--- a/src/HOL/Infinite_Set.thy	Fri Mar 24 19:30:01 2006 +0100
+++ b/src/HOL/Infinite_Set.thy	Sat Mar 25 18:16:07 2006 +0100
@@ -13,8 +13,12 @@
 
 text {* Some elementary facts about infinite sets, by Stefan Merz. *}
 
+syntax infinite :: "'a set \<Rightarrow> bool"
+translations "infinite S" == "\<not> finite S"
+(* doesnt work:
 abbreviation (output)
-  "infinite S = (S \<notin> Finites)"
+  "infinite S = (\<not> finite S)"
+*)
 
 text {*
   Infinite sets are non-empty, and if we remove some elements