src/HOL/Analysis/Complex_Analysis_Basics.thy

       then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h"
         by (simp add: norm_mult [symmetric] field_simps)
     qed
   } note ** = this
   show ?thesis
-  unfolding has_field_derivative_def
+    unfolding has_field_derivative_def
   proof (rule has_derivative_sequence [OF cvs _ _ x])
-    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
-      by (metis has_field_derivative_def df)
-  next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
+  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
     by (rule tf)
-  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
+  next show "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
     by (blast intro: **)
-  qed
+  qed (metis has_field_derivative_def df)
 qed
 
 lemma has_complex_derivative_series:
   fixes s :: "complex set"
   assumes cvs: "convex s"

     assume "x \<in> s"
     then show "((f n) has_derivative (\<lambda>z. z * f' n x)) (at x within s)"
       by (metis df has_field_derivative_def mult_commute_abs)
   next show " ((\<lambda>n. f n x) sums l)"
     by (rule sf)
-  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
+  next show "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
     by (blast intro: **)
   qed
 qed
 
 

   fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
   assumes "convex s" "open s"
   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
-  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
+  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
 proof -
   from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     unfolding uniformly_convergent_on_def by blast
   from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open)
   have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
     by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
   then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
     "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
-  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
     by (simp add: has_field_derivative_def s)
   have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
     by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
        (insert g, auto simp: sums_iff)
   thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
     by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
 qed
-
-lemma field_differentiable_series':
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
-  assumes "convex s" "open s"
-  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
-  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
-  shows   "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x0)"
-  using field_differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
 
 subsection\<open>Bound theorem\<close>
 
 lemma field_differentiable_bound:
   fixes s :: "'a::real_normed_field set"