src/HOL/Analysis/Elementary_Topology.thy

--- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -1325,9 +1325,6 @@
 
 subsection \<open>Limits\<close>
 
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
-  by (rule topological_tendstoI) (auto elim: eventually_mono)
-
 text \<open>The expected monotonicity property.\<close>
 
 lemma Lim_Un: