src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy

 qed
 
 (** Existence of a primitive.*)
 
 lemma holomorphic_starlike_primitive:
+  fixes f :: "complex \<Rightarrow> complex"
   assumes contf: "continuous_on s f"
       and s: "starlike s" and os: "open s"
       and k: "finite k"
       and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f complex_differentiable at x"
     shows "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x)"

   apply (simp_all add: ex_in_conv [symmetric])
   apply (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3)
   done
 
 lemma holomorphic_convex_primitive:
+  fixes f :: "complex \<Rightarrow> complex"
+  shows
   "\<lbrakk>convex s; finite k; continuous_on s f;
     \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
    \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
 apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
 prefer 3