diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -510,7 +510,7 @@
     by (simp add: fact_prod)
     (subst prod_dividef [symmetric], simp_all add: field_simps)
   also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
-    by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift)
+    by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)
   also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)"
     unfolding pochhammer_prod
     by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
@@ -535,7 +535,7 @@
   proof eventually_elim
     fix n :: nat assume n: "n > 0"
     have "(\<Sum>k<n. ?f k) = (\<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k))"
-      by (subst atLeast0LessThan [symmetric], subst sum_shift_bounds_Suc_ivl [symmetric],
+      by (subst atLeast0LessThan [symmetric], subst sum.shift_bounds_Suc_ivl [symmetric],
           subst atLeastLessThanSuc_atLeastAtMost) simp_all
     also have "\<dots> = z * of_real (harm n) - (\<Sum>k=1..n. ln (1 + z / of_nat k))"
       by (simp add: harm_def sum_subtractf sum_distrib_left divide_inverse)
@@ -653,7 +653,7 @@
     also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
       by (rule sum.union_disjoint) auto
     also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
-      using sum_shift_bounds_nat_ivl [of f 0 k m] by simp
+      using sum.shift_bounds_nat_ivl [of f 0 k m] by simp
     finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan)
   qed
   finally have "(\<lambda>a. sum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. sum f {..<m + k})"
@@ -2485,7 +2485,7 @@
   also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
     by (intro prod.cong) (simp_all add: divide_simps)
   also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
-    by (induction n) (simp_all add: prod_nat_ivl_Suc' divide_simps)
+    by (induction n) (simp_all add: prod.nat_ivl_Suc' divide_simps)
   finally show ?thesis ..
 qed
 
@@ -2515,8 +2515,13 @@
          (simp_all add: Gamma_series_euler'_def prod.distrib
                         prod_inversef[symmetric] divide_inverse)
     also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
-      by (cases n) (simp_all add: pochhammer_prod fact_prod atLeastLessThanSuc_atLeastAtMost
-        prod_dividef [symmetric] field_simps prod.atLeast_Suc_atMost_Suc_shift)
+    proof (cases n)
+      case (Suc n')
+      then show ?thesis
+        unfolding pochhammer_prod fact_prod
+        by (simp add:  atLeastLessThanSuc_atLeastAtMost field_simps prod_dividef 
+                  prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)
+    qed auto
     also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
     finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
   qed
@@ -2561,7 +2566,7 @@
   have "(\<lambda>n. \<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k)) \<longlonglongrightarrow> ln_Gamma z + euler_mascheroni * z + ln z"
     using ln_Gamma_series'_aux[OF False]
     by (simp only: atLeastLessThanSuc_atLeastAtMost [symmetric] One_nat_def
-                   sum_shift_bounds_Suc_ivl sums_def atLeast0LessThan)
+                   sum.shift_bounds_Suc_ivl sums_def atLeast0LessThan)
   from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z"
     by (simp add: exp_add exp_sum exp_diff mult_ac Gamma_complex_altdef A)
   from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z
@@ -2842,7 +2847,7 @@
       also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
       also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
         by (simp add: divide_simps pochhammer_rec
-              prod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
+              prod.shift_bounds_cl_Suc_ivl del: of_nat_Suc)
       finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
         by simp
     qed (simp_all add: bounded_bilinear_mult)
@@ -3248,7 +3253,7 @@
     have "(\<lambda>n. P x n - P x (Suc n)) sums (P x 0 - sin (pi * x) / (pi * x))"
       unfolding P_def using x by (intro telescope_sums' sin_product_formula_real')
     also have "(\<lambda>n. P x n - P x (Suc n)) = (\<lambda>n. (x^2 / of_nat (Suc n)^2) * P x n)"
-      unfolding P_def by (simp add: prod_nat_ivl_Suc' algebra_simps)
+      unfolding P_def by (simp add: prod.nat_ivl_Suc' algebra_simps)
     also have "P x 0 = 1" by (simp add: P_def)
     finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" .
     from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp