changeset 19328 | e090c939a29b |
parent 19313 | 45c9fc22904b |
child 19363 | 667b5ea637dd |
--- 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