equal
deleted
inserted
replaced
32 by (rtac succ_leE 1); |
32 by (rtac succ_leE 1); |
33 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
33 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
34 qed "gt_pred"; |
34 qed "gt_pred"; |
35 |
35 |
36 |
36 |
37 Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P]; |
37 Addsimps [not_lt_iff_le, if_P, if_not_P]; |
38 |
38 |
39 |
39 |
40 (* ------------------------------------------------------------------------- *) |
40 (* ------------------------------------------------------------------------- *) |
41 (* lift_rec equality rules *) |
41 (* lift_rec equality rules *) |
42 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |