--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Dec 27 19:48:28 2018 +0100
@@ -212,7 +212,7 @@
lemma real_lim:
fixes l::complex
- assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
+ assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
shows "l \<in> \<real>"
proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
show "eventually (\<lambda>x. f x \<in> \<real>) F"