author | huffman |
Thu, 20 Oct 2011 22:02:49 +0200 | |
changeset 45220 | 1c9f10955ec1 |
parent 45219 | 29f6e990674d (diff) |
parent 45218 | f115540543d8 (current diff) |
child 45221 | 3eadb9b6a055 |
child 45224 | b1d5b3820d82 |
--- a/src/HOL/Int.thy Thu Oct 20 12:30:43 2011 -0400 +++ b/src/HOL/Int.thy Thu Oct 20 22:02:49 2011 +0200 @@ -1543,7 +1543,7 @@ lemmas int_arith_rules = neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1 minus_zero diff_minus left_minus right_minus - mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right + mult_zero_left mult_zero_right mult_1_left mult_1_right mult_minus_left mult_minus_right minus_add_distrib minus_minus mult_assoc of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult