equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Implementation of natural numbers by target-language integers *} |
6 header {* Implementation of natural numbers by target-language integers *} |
7 |
7 |
8 theory Efficient_Nat |
8 theory Efficient_Nat |
9 imports Main Code_Integer Code_Index |
9 imports Code_Integer Code_Index |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 When generating code for functions on natural numbers, the |
13 When generating code for functions on natural numbers, the |
14 canonical representation using @{term "0::nat"} and |
14 canonical representation using @{term "0::nat"} and |