equal
deleted
inserted
replaced
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 imports Main |
10 imports PreList |
11 begin |
11 begin |
12 |
12 |
13 text{* |
13 text{* |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition |
15 and proofs are from \cite[page 85]{Oberschelp:1993}. |
15 and proofs are from \cite[page 85]{Oberschelp:1993}. |