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