equal
deleted
inserted
replaced
3 Author: Tobias Nipkow and Markus Wenzel |
3 Author: Tobias Nipkow and Markus Wenzel |
4 *) |
4 *) |
5 |
5 |
6 header {* More arithmetic on natural numbers *} |
6 header {* More arithmetic on natural numbers *} |
7 |
7 |
8 theory NatArith = Nat |
8 theory NatArith |
9 files "arith_data.ML": |
9 import Nat |
|
10 files "arith_data.ML" |
|
11 begin |
10 |
12 |
11 setup arith_setup |
13 setup arith_setup |
12 |
14 |
13 |
15 |
14 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" |
16 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" |