src/HOL/Num.thy
changeset 47227 bc18fa07053b
parent 47226 ea712316fc87
child 47228 4f4d85c3516f
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 15:56:12 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 16:43:07 2012 +0200
     1.3 @@ -507,7 +507,7 @@
     1.4  lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
     1.5    apply (induct n rule: num_induct)
     1.6    apply (simp add: numeral_One)
     1.7 -  apply (simp add: mult_inc numeral_inc numeral_add numeral_inc right_distrib)
     1.8 +  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
     1.9    done
    1.10  
    1.11  lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"