--- a/src/HOL/Topological_Spaces.thy Wed Jan 20 20:19:05 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Jan 22 16:00:03 2016 +0000
@@ -1076,6 +1076,9 @@
lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
+lemma lim_const [simp]: "lim (\<lambda>m. a) = a"
+ by (simp add: limI)
+
subsubsection\<open>Increasing and Decreasing Series\<close>
lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"