equal
deleted
inserted
replaced
4 |
4 |
5 header {* Encoding (almost) everything into natural numbers *} |
5 header {* Encoding (almost) everything into natural numbers *} |
6 |
6 |
7 theory Countable |
7 theory Countable |
8 imports |
8 imports |
9 Plain |
|
10 "~~/src/HOL/List" |
9 "~~/src/HOL/List" |
11 "~~/src/HOL/Hilbert_Choice" |
10 "~~/src/HOL/Hilbert_Choice" |
12 "~~/src/HOL/Nat_Int_Bij" |
11 "~~/src/HOL/Nat_Int_Bij" |
13 "~~/src/HOL/Rational" |
12 "~~/src/HOL/Rational" |
|
13 Main |
14 begin |
14 begin |
15 |
15 |
16 subsection {* The class of countable types *} |
16 subsection {* The class of countable types *} |
17 |
17 |
18 class countable = |
18 class countable = |