src/HOL/Library/Extended_Real.thy

   shows "(f \<longlongrightarrow> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
   unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
   using Liminf_le_Limsup[OF assms, of f]
   by auto
 
-lemma convergent_ereal: -- \<open>RENAME\<close>
+lemma convergent_ereal: \<comment> \<open>RENAME\<close>
   fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   by (auto simp: convergent_def)