# HG changeset patch
# User huffman
# Date 1333118587 -7200
# Node ID bc18fa07053b55b3cbff739f3e980691e453b2ba
# Parent  ea712316fc871b424b4a1cf530d7c90042a4eed0
tuned proof

diff -r ea712316fc87 -r bc18fa07053b src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 30 15:56:12 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 16:43:07 2012 +0200
@@ -507,7 +507,7 @@
 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   apply (induct n rule: num_induct)
   apply (simp add: numeral_One)
-  apply (simp add: mult_inc numeral_inc numeral_add numeral_inc right_distrib)
+  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
   done
 
 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"