src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 69508 2a4c8a2a3f8e
parent 69286 e4d5a07fecb6
child 69529 4ab9657b3257
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Dec 26 20:57:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Dec 27 19:48:28 2018 +0100
     1.3 @@ -212,7 +212,7 @@
     1.4  
     1.5  lemma real_lim:
     1.6    fixes l::complex
     1.7 -  assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
     1.8 +  assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
     1.9    shows  "l \<in> \<real>"
    1.10  proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
    1.11    show "eventually (\<lambda>x. f x \<in> \<real>) F"