| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 19736 | d8d0f8f51d69 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Pairs of Natural Numbers *} |
7 header {* Pairs of Natural Numbers *} |
8 |
8 |
9 theory NatPair |
9 theory NatPair |
10 import Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 text{* |
13 text{* |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text |
15 \<nat>}. Definition and proofs are from \cite[page |
15 \<nat>}. Definition and proofs are from \cite[page |