# HG changeset patch
# User huffman
# Date 1319124434 -7200
# Node ID 29f6e990674d4b53a0f3a50df9770b9658eea784
# Parent  c4fab1099cd0b10ef8426436c93cd5bfad4205d0
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

diff -r c4fab1099cd0 -r 29f6e990674d src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 20 10:44:00 2011 +0200
+++ b/src/HOL/Int.thy	Thu Oct 20 17:27:14 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