# HG changeset patch
# User blanchet
# Date 1494436280 -7200
# Node ID d53be22028599c14e3219ac23e1c40b61e334a35
# Parent  ed705d6a6a632efd32251fd057a4cc091f6ea92b
tuning

diff -r ed705d6a6a63 -r d53be2202859 src/HOL/Library/Cancellation.thy
--- 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>