equal
deleted
inserted
replaced
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 Plain List Hilbert_Choice |
9 imports Plain "~~/src/HOL/List" "~~/src/HOL/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 + |