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 non-empty, and if we remove some elements |
21 Infinite sets are non-empty, 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 *} |