equal
deleted
inserted
replaced
7 theory NatArith = Nat |
7 theory NatArith = Nat |
8 files "arith_data.ML": |
8 files "arith_data.ML": |
9 |
9 |
10 setup arith_setup |
10 setup arith_setup |
11 |
11 |
12 lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)" |
12 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" |
13 apply (simp add: less_eq reflcl_trancl [THEN sym] |
13 apply (simp add: less_eq reflcl_trancl [symmetric] |
14 del: reflcl_trancl) |
14 del: reflcl_trancl) |
15 by arith |
15 by arith |
16 |
16 |
17 (*elimination of `-' on nat*) |
17 (*elimination of `-' on nat*) |
18 lemma nat_diff_split: |
18 lemma nat_diff_split: |