1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 07:45:22 2011 -0700
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 08:39:43 2011 -0700
     1.3 @@ -839,7 +839,8 @@
     1.4        cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
     1.5        + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
     1.6        (is "_ = ?SUM + ?rest / ?fact * ?pow")
     1.7 -      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
     1.8 +      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
     1.9 +      unfolding cos_coeff_def by auto
    1.10  
    1.11      have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
    1.12      also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
    1.13 @@ -951,7 +952,8 @@
    1.14        sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
    1.15        + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
    1.16        (is "_ = ?SUM + ?rest / ?fact * ?pow")
    1.17 -      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
    1.18 +      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
    1.19 +      unfolding sin_coeff_def by auto
    1.20  
    1.21      have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
    1.22      moreover