src/HOL/Decision_Procs/Approximation.thy
changeset 31790 05c92381363c
parent 31508 1ea1c70aba00
child 31809 06372924e86c
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -422,7 +422,7 @@
     1.4  
     1.5      have "\<bar> real x \<bar> \<le> 1"  using `0 \<le> real x` `real x \<le> 1` by auto
     1.6      from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
     1.7 -    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_plus1  .
     1.8 +    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1  .
     1.9    qed auto
    1.10    note arctan_bounds = this[unfolded atLeastAtMost_iff]
    1.11  
    1.12 @@ -1179,7 +1179,7 @@
    1.13  proof (induct n arbitrary: x)
    1.14    case (Suc n)
    1.15    have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
    1.16 -    unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    1.17 +    unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    1.18    show ?case unfolding split_pi_off using Suc by auto
    1.19  qed auto
    1.20  
    1.21 @@ -1676,7 +1676,7 @@
    1.22      using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
    1.23  
    1.24    have "norm x < 1" using assms by auto
    1.25 -  have "?a ----> 0" unfolding Suc_plus1[symmetric] inverse_eq_divide[symmetric] 
    1.26 +  have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] 
    1.27      using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
    1.28    { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
    1.29    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]