| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15234 | ec91a90c604e |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Integer arithmetic *} |
6 header {* Integer arithmetic *} |
7 |
7 |
8 theory IntArith |
8 theory IntArith |
9 import Numeral |
9 imports Numeral |
10 files ("int_arith1.ML") |
10 files ("int_arith1.ML") |
11 begin |
11 begin |
12 |
12 |
13 text{*Duplicate: can't understand why it's necessary*} |
13 text{*Duplicate: can't understand why it's necessary*} |
14 declare numeral_0_eq_0 [simp] |
14 declare numeral_0_eq_0 [simp] |