src/HOL/Nat.thy
changeset 49962 a8cc904a6820
parent 49834 b27bbb021df1
child 51173 3cbb4e95a565
     1.1 --- a/src/HOL/Nat.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -312,7 +312,7 @@
     1.4    by (rule mult_commute)
     1.5  
     1.6  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
     1.7 -  by (rule right_distrib)
     1.8 +  by (rule distrib_left)
     1.9  
    1.10  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
    1.11    by (induct m) auto
    1.12 @@ -1342,7 +1342,7 @@
    1.13    by (induct m) (simp_all add: add_ac)
    1.14  
    1.15  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    1.16 -  by (induct m) (simp_all add: add_ac left_distrib)
    1.17 +  by (induct m) (simp_all add: add_ac distrib_right)
    1.18  
    1.19  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.20    "of_nat_aux inc 0 i = i"