equal
deleted
inserted
replaced
5 |
5 |
6 header {*Further Arithmetic Facts Concerning the Natural Numbers*} |
6 header {*Further Arithmetic Facts Concerning the Natural Numbers*} |
7 |
7 |
8 theory NatArith |
8 theory NatArith |
9 imports Nat |
9 imports Nat |
10 files "arith_data.ML" |
10 uses "arith_data.ML" |
11 begin |
11 begin |
12 |
12 |
13 setup arith_setup |
13 setup arith_setup |
14 |
14 |
15 text{*The following proofs may rely on the arithmetic proof procedures.*} |
15 text{*The following proofs may rely on the arithmetic proof procedures.*} |