# HG changeset patch
# User nipkow
# Date 1143022498 -3600
# Node ID 45c9fc22904be28cb423d9d2715159aa872920ae
# Parent  bb3cbf03a021badce756d0bbf0f3c4870069548e
translations -> abbreviations (a cool feature)

diff -r bb3cbf03a021 -r 45c9fc22904b src/HOL/Finite_Set.thy
--- 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
diff -r bb3cbf03a021 -r 45c9fc22904b src/HOL/Infinite_Set.thy
--- 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