--- a/src/HOL/Library/Extended_Real.thy Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed May 25 11:49:40 2016 +0200
@@ -3552,7 +3552,7 @@
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]