--- a/src/HOL/Analysis/ex/Approximations.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy Wed Apr 10 13:34:55 2019 +0100
@@ -27,7 +27,7 @@
{
fix m :: nat
have "(\<Sum>k<Suc m. f k * x^k) = f 0 + (\<Sum>k=Suc 0..<Suc m. f k * x^k)"
- by (subst atLeast0LessThan [symmetric], subst sum_head_upt_Suc) simp_all
+ by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
by (subst sum_shift_bounds_Suc_ivl)
(simp add: sum_distrib_right algebra_simps atLeast0LessThan power_commutes)
@@ -420,7 +420,7 @@
fix m :: nat
have "(\<Sum>k<Suc m. inverse (f k * x^k)) =
inverse (f 0) + (\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k))"
- by (subst atLeast0LessThan [symmetric], subst sum_head_upt_Suc) simp_all
+ by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k)) = (\<Sum>k<m. inverse (f (k+1) * x^k)) / x"
by (subst sum_shift_bounds_Suc_ivl)
(simp add: sum_distrib_left divide_inverse algebra_simps