changed abbreviation for "infinite" back to translation because
something didn't work during (output).
--- 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