equal
deleted
inserted
replaced
6 Binary arithmetic for the natural numbers |
6 Binary arithmetic for the natural numbers |
7 |
7 |
8 This case is simply reduced to that for the non-negative integers |
8 This case is simply reduced to that for the non-negative integers |
9 *) |
9 *) |
10 |
10 |
11 NatBin = IntPower + |
11 theory NatBin = IntPower |
|
12 files ("nat_bin.ML"): |
12 |
13 |
13 instance |
14 instance nat :: number .. |
14 nat :: number |
|
15 |
15 |
16 defs |
16 defs |
17 nat_number_of_def |
17 nat_number_of_def: |
18 "number_of v == nat (number_of v)" |
18 "number_of v == nat (number_of v)" |
19 (*::bin=>nat ::bin=>int*) |
19 (*::bin=>nat ::bin=>int*) |
20 |
20 |
|
21 use "nat_bin.ML" setup nat_bin_arith_setup |
|
22 |
21 end |
23 end |