| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15234 | ec91a90c604e |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Binary arithmetic for the natural numbers *} |
7 header {* Binary arithmetic for the natural numbers *} |
8 |
8 |
9 theory NatBin |
9 theory NatBin |
10 import IntDiv |
10 imports IntDiv |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Arithmetic for naturals is reduced to that for the non-negative integers. |
14 Arithmetic for naturals is reduced to that for the non-negative integers. |
15 *} |
15 *} |