Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof
authorhuffman
Fri, 30 Mar 2012 16:43:07 +0200
changeset 47227 bc18fa07053b
parent 47226 ea712316fc87
child 47228 4f4d85c3516f
tuned proof
src/HOL/Num.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle