| changeset 11464 | ddea204de5bc |
| parent 10574 | 8f98f0301d67 |
| child 11468 | 02cd5d5bc497 |
| 11463:96b5b27da55c | 11464:ddea204de5bc |
|---|---|
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 axioms |
|
22 neg_number_of_bin_pred_iff_0: |
|
23 "neg (number_of (bin_pred v)) = (number_of v = (0::nat))" |
|
24 |
|
21 use "nat_bin.ML" setup nat_bin_arith_setup |
25 use "nat_bin.ML" setup nat_bin_arith_setup |
22 |
26 |
23 end |
27 end |