--- 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