
diff -r d3d2b78b1c19 -r a8cc904a6820 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/MacLaurin.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -415,7 +415,7 @@
 lemma sin_expansion_lemma:
      "sin (x + real (Suc m) * pi / 2) =
       cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto)
 
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
@@ -489,7 +489,7 @@
 
 lemma cos_expansion_lemma:
   "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
 
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &




