--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 14:34:45 2016 +0000
@@ -2678,6 +2678,7 @@
(** 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"
@@ -2796,6 +2797,8 @@
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)"