diff -r f17602cbf76a -r 1d066f6ab25d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Apr 14 12:17:44 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Apr 14 15:48:11 2016 +0200
@@ -3547,7 +3547,7 @@
   using Liminf_le_Limsup[OF assms, of f]
   by auto
 
-lemma convergent_ereal:
+lemma convergent_ereal: -- \<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]