diff -r 5574d504cf36 -r 4ab9657b3257 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Dec 29 15:43:53 2018 +0100
@@ -552,7 +552,7 @@
   shows "uniformly_convergent_on (ball z d)
             (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
            (is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)")
-proof (rule weierstrass_m_test'_ev)
+proof (rule Weierstrass_m_test'_ev)
   {
     fix t assume t: "t \<in> ball z d"
     have "norm z = norm (t + (z - t))" by simp
@@ -665,7 +665,7 @@
   fixes z :: "'a :: {real_normed_field,banach}"
   assumes z: "z \<noteq> 0" and n: "n \<ge> 2"
   shows "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)^n))"
-proof (rule weierstrass_m_test'_ev)
+proof (rule Weierstrass_m_test'_ev)
   define e where "e = (1 + d / norm z)"
   define m where "m = nat \<lceil>norm z * e\<rceil>"
   {
@@ -2528,29 +2528,29 @@
 
 subsubsection \<open>Weierstrass form\<close>
 
-definition Gamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
-  "Gamma_series_weierstrass z n =
+definition Gamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
+  "Gamma_series_Weierstrass z n =
      exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
 
 definition%unimportant
-  rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
-  "rGamma_series_weierstrass z n =
+  rGamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
+  "rGamma_series_Weierstrass z n =
      exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
 
-lemma Gamma_series_weierstrass_nonpos_Ints:
-  "eventually (\<lambda>k. Gamma_series_weierstrass (- of_nat n) k = 0) sequentially"
-  using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_weierstrass_def)
-
-lemma rGamma_series_weierstrass_nonpos_Ints:
-  "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
-  using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
-
-theorem Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
+lemma Gamma_series_Weierstrass_nonpos_Ints:
+  "eventually (\<lambda>k. Gamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
+  using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_Weierstrass_def)
+
+lemma rGamma_series_Weierstrass_nonpos_Ints:
+  "eventually (\<lambda>k. rGamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
+  using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_Weierstrass_def)
+
+theorem Gamma_Weierstrass_complex: "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   case True
   then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
-  also from True have "Gamma_series_weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
-    by (simp add: tendsto_cong[OF Gamma_series_weierstrass_nonpos_Ints] Gamma_nonpos_Int)
+  also from True have "Gamma_series_Weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
+    by (simp add: tendsto_cong[OF Gamma_series_Weierstrass_nonpos_Ints] Gamma_nonpos_Int)
   finally show ?thesis .
 next
   case False
@@ -2565,32 +2565,32 @@
   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
-    show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z"
-    by (simp add: exp_minus divide_simps Gamma_series_weierstrass_def [abs_def])
+    show "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma z"
+    by (simp add: exp_minus divide_simps Gamma_series_Weierstrass_def [abs_def])
 qed
 
 lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F"
   by (rule tendsto_of_real_iff)
 
-lemma Gamma_weierstrass_real: "Gamma_series_weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
-  using Gamma_weierstrass_complex[of "of_real x"] unfolding Gamma_series_weierstrass_def[abs_def]
+lemma Gamma_Weierstrass_real: "Gamma_series_Weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
+  using Gamma_Weierstrass_complex[of "of_real x"] unfolding Gamma_series_Weierstrass_def[abs_def]
   by (subst tendsto_complex_of_real_iff [symmetric])
      (simp_all add: exp_of_real[symmetric] Gamma_complex_of_real)
 
-lemma rGamma_weierstrass_complex: "rGamma_series_weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
+lemma rGamma_Weierstrass_complex: "rGamma_series_Weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   case True
   then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
-  also from True have "rGamma_series_weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
-    by (simp add: tendsto_cong[OF rGamma_series_weierstrass_nonpos_Ints] rGamma_nonpos_Int)
+  also from True have "rGamma_series_Weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
+    by (simp add: tendsto_cong[OF rGamma_series_Weierstrass_nonpos_Ints] rGamma_nonpos_Int)
   finally show ?thesis .
 next
   case False
-  have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
-    by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
+  have "rGamma_series_Weierstrass z = (\<lambda>n. inverse (Gamma_series_Weierstrass z n))"
+    by (simp add: rGamma_series_Weierstrass_def[abs_def] Gamma_series_Weierstrass_def
                   exp_minus divide_inverse prod_inversef[symmetric] mult_ac)
   also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
-    by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
+    by (intro tendsto_intros Gamma_Weierstrass_complex) (simp add: Gamma_eq_zero_iff)
   finally show ?thesis by (simp add: Gamma_def)
 qed
 
@@ -3175,17 +3175,17 @@
   fixes z :: complex
   shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
 proof -
-  let ?f = "rGamma_series_weierstrass"
+  let ?f = "rGamma_series_Weierstrass"
   have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (- z) n))
             \<longlonglongrightarrow> (- of_real pi * inverse z) * (rGamma z * rGamma (- z))"
-    by (intro tendsto_intros rGamma_weierstrass_complex)
+    by (intro tendsto_intros rGamma_Weierstrass_complex)
   also have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (-z) n)) =
                     (\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2))"
   proof
     fix n :: nat
     have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
               of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
-      by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
+      by (simp add: rGamma_series_Weierstrass_def mult_ac exp_minus
                     divide_simps prod.distrib[symmetric] power2_eq_square)
     also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
                  (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
@@ -3257,7 +3257,7 @@
   have "continuous_on (ball 0 1) f"
   proof (rule uniform_limit_theorem; (intro always_eventually allI)?)
     show "uniform_limit (ball 0 1) (\<lambda>n x. \<Sum>k<n. P x k / of_nat (Suc k)^2) f sequentially"
-    proof (unfold f_def, rule weierstrass_m_test)
+    proof (unfold f_def, rule Weierstrass_m_test)
       fix n :: nat and x :: real assume x: "x \<in> ball 0 1"
       {
         fix k :: nat assume k: "k \<ge> 1"