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.
tuning
authorblanchet
Wed, 10 May 2017 19:11:20 +0200
changeset 65800 d53be2202859
parent 65799 ed705d6a6a63
child 65801 aeb776b5b054
tuning
src/HOL/Library/Cancellation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Cancellation.thy	Wed May 10 19:02:06 2017 +0200
+++ b/src/HOL/Library/Cancellation.thy	Wed May 10 19:11:20 2017 +0200
@@ -39,7 +39,7 @@
   by (induction n) auto
 
 lemma iterate_add_1: \<open>iterate_add n 1 = of_nat n\<close>
-  by (induction n) auto
+  using iterate_add_Numeral1 by auto
 
 lemma iterate_add_eq_add_iff1:
   \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>
isabelle