src/HOL/Transcendental.thy

   also have "\<dots> = (\<Sum>i\<le>n. \<Sum>j<i. a i * (x - y) * (y^(i - Suc j) * x^j))"
     by (simp add: sum_distrib_left)
   also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
     by (simp add: sum.Sigma)
   also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
-    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
     by (simp add: sum.Sigma)
   also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
     by (simp add: sum_distrib_left mult_ac)
   finally show ?thesis .

     have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
       apply (auto simp: bij_betw_def inj_on_def)
       apply (rule_tac x="x + Suc j" in image_eqI, auto)
       done
     then show ?thesis
-      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   qed
   then show ?thesis
     by (simp add: polyfun_diff [OF assms] sum_distrib_right)
 qed