# HG changeset patch
# User nipkow
# Date 1143306967 -3600
# Node ID e090c939a29b380eedfc2ec5842dacbcbecd2828
# Parent  4565e230e6eb44136c5cd231ef01215e9a758dc0
changed abbreviation for "infinite" back to translation because
something didn't work during (output).

diff -r 4565e230e6eb -r e090c939a29b src/HOL/Infinite_Set.thy
--- 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