| changeset 27368 | 9f90ac19e32b |
| parent 26585 | 3bf2ebb7148e |
| child 27487 | c8a6ce181805 |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Encoding (almost) everything into natural numbers *} |
6 header {* Encoding (almost) everything into natural numbers *} |
7 |
7 |
8 theory Countable |
8 theory Countable |
9 imports Finite_Set List Hilbert_Choice |
9 imports Plain List Hilbert_Choice |
10 begin |
10 begin |
11 |
11 |
12 subsection {* The class of countable types *} |
12 subsection {* The class of countable types *} |
13 |
13 |
14 class countable = itself + |
14 class countable = itself + |