removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
authorhuffman
Thu Oct 20 17:27:14 2011 +0200 (2011-10-20)
changeset 4521929f6e990674d
parent 45217 c4fab1099cd0
child 45220 1c9f10955ec1
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Thu Oct 20 10:44:00 2011 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Oct 20 17:27:14 2011 +0200
     1.3 @@ -1543,7 +1543,7 @@
     1.4  lemmas int_arith_rules =
     1.5    neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
     1.6    minus_zero diff_minus left_minus right_minus
     1.7 -  mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
     1.8 +  mult_zero_left mult_zero_right mult_1_left mult_1_right
     1.9    mult_minus_left mult_minus_right
    1.10    minus_add_distrib minus_minus mult_assoc
    1.11    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult