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]
```