src/HOL/Analysis/Complex_Transcendental.thy
changeset 66793 deabce3ccf1f
parent 66611 c375b64a6c24
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -1233,7 +1233,7 @@
     1.4  lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
     1.5    by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
     1.6  
     1.7 -lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
     1.8 +lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
     1.9    by (simp add: field_differentiable_within_Ln holomorphic_on_def)
    1.10  
    1.11  lemma divide_ln_mono: