equal
deleted
inserted
replaced
4 Copyright 1999 University of Cambridge |
4 Copyright 1999 University of Cambridge |
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 = IntDiv: |
9 theory NatBin |
|
10 import IntDiv |
|
11 begin |
10 |
12 |
11 text {* |
13 text {* |
12 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. |
13 *} |
15 *} |
14 |
16 |