| changeset 12023 | d982f98e0f0d |
| parent 11868 | 56db9f3a6b3e |
| child 13575 | ecb6ecd9af13 |
| 12022:9c3377b133c0 | 12023:d982f98e0f0d |
|---|---|
1 |
|
2 header {* Integer arithmetic *} |
|
3 |
|
1 theory IntArith = Bin |
4 theory IntArith = Bin |
2 files ("int_arith1.ML") ("int_arith2.ML"): |
5 files ("int_arith1.ML") ("int_arith2.ML"): |
3 |
6 |
4 use "int_arith1.ML" setup int_arith_setup |
7 use "int_arith1.ML" |
5 use "int_arith2.ML" lemmas [arith_split] = zabs_split |
8 setup int_arith_setup |
9 use "int_arith2.ML" |
|
10 declare zabs_split [arith_split] |
|
11 |
|
6 end |
12 end |