src/HOL/Library/Liminf_Limsup.thy
changeset 61969 e01015e49041
parent 61880 ff4d33058566
child 61973 0c7e865fa7cb
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 29 23:04:53 2015 +0100
@@ -365,9 +365,9 @@
 
 lemma lim_increasing_cl:
   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
 proof
-  show "f ----> (SUP n. f n)"
+  show "f \<longlonglongrightarrow> (SUP n. f n)"
     using assms
     by (intro increasing_tendsto)
        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
@@ -375,9 +375,9 @@
 
 lemma lim_decreasing_cl:
   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
 proof
-  show "f ----> (INF n. f n)"
+  show "f \<longlonglongrightarrow> (INF n. f n)"
     using assms
     by (intro decreasing_tendsto)
        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
@@ -385,7 +385,7 @@
 
 lemma compact_complete_linorder:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
+  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
 proof -
   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
     using seq_monosub[of X]
@@ -393,7 +393,7 @@
     by auto
   then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
     by (auto simp add: monoseq_def)
-  then obtain l where "(X \<circ> r) ----> l"
+  then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
      by auto
   then show ?thesis