equal
deleted
inserted
replaced
11 
11 
12 subsection "Infinite Sets" 
12 subsection "Infinite Sets" 
13 
13 
14 text {* Some elementary facts about infinite sets, by Stefan Merz. *} 
14 text {* Some elementary facts about infinite sets, by Stefan Merz. *} 
15 
15 
16 syntax infinite :: "'a set \<Rightarrow> bool" 
16 abbreviation 
17 translations "infinite S" == "\<not> finite S" 
17 infinite :: "'a set \<Rightarrow> bool" 
18 (* doesnt work: 
18 "infinite S == \<not> finite S" 
19 abbreviation (output) 

20 "infinite S = (\<not> finite S)" 

21 *) 

22 
19 
23 text {* 
20 text {* 
24 Infinite sets are nonempty, and if we remove some elements 
21 Infinite sets are nonempty, and if we remove some elements 
25 from an infinite set, the result is still infinite. 
22 from an infinite set, the result is still infinite. 
26 *} 
23 *} 