diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Infinite_Set.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -13,12 +13,9 @@
 
 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 = (\<not> finite S)"
-*)
+abbreviation
+  infinite :: "'a set \<Rightarrow> bool"
+  "infinite S == \<not> finite S"
 
 text {*
   Infinite sets are non-empty, and if we remove some elements