--- a/src/HOL/Finite_Set.thy Tue Mar 21 15:38:53 2006 +0100
+++ b/src/HOL/Finite_Set.thy Wed Mar 22 11:14:58 2006 +0100
@@ -13,10 +13,8 @@
subsection {* Definition and basic properties *}
consts Finites :: "'a set set"
-syntax
- finite :: "'a set => bool"
-translations
- "finite A" == "A : Finites"
+abbreviation (output)
+ "finite A = (A : Finites)"
inductive Finites
intros
--- 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