--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Nov 17 12:32:08 2015 +0000
@@ -28,10 +28,10 @@
apply (simp only: abs_diff_le_iff)
apply (rule sin_pi6_straddle, simp_all)
using Taylor_sin [of "1686629713/3221225472" 11]
- apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
+ apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral power_divide)
apply (simp only: pos_le_divide_eq [symmetric])
using Taylor_sin [of "6746518853/12884901888" 11]
- apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
+ apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral power_divide)
apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
done