1.1 --- a/src/HOL/MacLaurin.thy	Thu May 14 08:22:07 2009 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Thu May 14 15:39:15 2009 +0200
     1.3 @@ -552,10 +552,6 @@
     1.4      "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
     1.5  by auto
     1.6  
     1.7 -text {* TODO: move to Parity.thy *}
     1.8 -lemma nat_odd_1 [simp]: "odd (1::nat)"
     1.9 -  unfolding even_nat_def by simp
    1.10 -
    1.11  lemma Maclaurin_sin_bound:
    1.12    "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.13    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"