equal
deleted
inserted
replaced
3 Authors: Larry Paulson and Tobias Nipkow |
3 Authors: Larry Paulson and Tobias Nipkow |
4 *) |
4 *) |
5 |
5 |
6 header {* Integer arithmetic *} |
6 header {* Integer arithmetic *} |
7 |
7 |
8 theory IntArith = Numeral |
8 theory IntArith |
9 files ("int_arith1.ML"): |
9 import Numeral |
|
10 files ("int_arith1.ML") |
|
11 begin |
10 |
12 |
11 text{*Duplicate: can't understand why it's necessary*} |
13 text{*Duplicate: can't understand why it's necessary*} |
12 declare numeral_0_eq_0 [simp] |
14 declare numeral_0_eq_0 [simp] |
13 |
15 |
14 subsection{*Instantiating Binary Arithmetic for the Integers*} |
16 subsection{*Instantiating Binary Arithmetic for the Integers*} |