equal
deleted
inserted
replaced
1541 subsection {* Setting up simplification procedures *} |
1541 subsection {* Setting up simplification procedures *} |
1542 |
1542 |
1543 lemmas int_arith_rules = |
1543 lemmas int_arith_rules = |
1544 neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1 |
1544 neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1 |
1545 minus_zero diff_minus left_minus right_minus |
1545 minus_zero diff_minus left_minus right_minus |
1546 mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right |
1546 mult_zero_left mult_zero_right mult_1_left mult_1_right |
1547 mult_minus_left mult_minus_right |
1547 mult_minus_left mult_minus_right |
1548 minus_add_distrib minus_minus mult_assoc |
1548 minus_add_distrib minus_minus mult_assoc |
1549 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
1549 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
1550 of_int_0 of_int_1 of_int_add of_int_mult |
1550 of_int_0 of_int_1 of_int_add of_int_mult |
1551 |
1551 |