src/HOL/Num.thy
changeset 49962 a8cc904a6820
parent 49690 a6814de45b69
child 50817 652731d92061
     1.1 --- a/src/HOL/Num.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4    "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
     1.5    "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
     1.6    by (simp_all add: num_eq_iff nat_of_num_add
     1.7 -    nat_of_num_mult left_distrib right_distrib)
     1.8 +    nat_of_num_mult distrib_right distrib_left)
     1.9  
    1.10  lemma eq_num_simps:
    1.11    "One = One \<longleftrightarrow> True"
    1.12 @@ -510,7 +510,7 @@
    1.13  lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
    1.14    apply (induct n rule: num_induct)
    1.15    apply (simp add: numeral_One)
    1.16 -  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
    1.17 +  apply (simp add: mult_inc numeral_inc numeral_add distrib_left)
    1.18    done
    1.19  
    1.20  lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
    1.21 @@ -532,10 +532,10 @@
    1.22      simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
    1.23  
    1.24  lemma mult_2: "2 * z = z + z"
    1.25 -  unfolding one_add_one [symmetric] left_distrib by simp
    1.26 +  unfolding one_add_one [symmetric] distrib_right by simp
    1.27  
    1.28  lemma mult_2_right: "z * 2 = z + z"
    1.29 -  unfolding one_add_one [symmetric] right_distrib by simp
    1.30 +  unfolding one_add_one [symmetric] distrib_left by simp
    1.31  
    1.32  end
    1.33