diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/MacLaurin.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -81,7 +81,7 @@
   prefer 2 apply simp
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
@@ -124,7 +124,7 @@
 
   have g2: "g 0 = 0 & g h = 0"
     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
-    apply (cut_tac n = m and k = 1 in sumr_offset2)
+    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
     done
 
@@ -144,7 +144,7 @@
     apply (simp add: m difg_def)
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
-    apply (insert sumr_offset4 [of 1])
+    apply (insert sumr_offset4 [of "Suc 0"])
     apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
     done
 
@@ -552,6 +552,10 @@
     "[|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"