changeset 21256 | 47195501ecf7 |
parent 21210 | c17fd2df4e9e |
child 21404 | eb85850d3eb7 |
21255:617fdb08abe9 | 21256:47195501ecf7 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Infinite Sets and Related Concepts *} |
6 header {* Infinite Sets and Related Concepts *} |
7 |
7 |
8 theory Infinite_Set |
8 theory Infinite_Set |
9 imports Hilbert_Choice Binomial |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 subsection "Infinite Sets" |
12 subsection "Infinite Sets" |
13 |
13 |
14 text {* |
14 text {* |