src/HOL/Decision_Procs/Approximation.thy
 changeset 44306 33572a766836 parent 44305 3bdc02eb1637 child 44349 f057535311c5
```     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