src/HOL/Library/Liminf_Limsup.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61245 b77bf45efe21
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section {* Liminf and Limsup on complete lattices *}
+section \<open>Liminf and Limsup on complete lattices\<close>
 
 theory Liminf_Limsup
 imports Complex_Main
@@ -30,7 +30,7 @@
   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
-subsubsection {* @{text Liminf} and @{text Limsup} *}
+subsubsection \<open>@{text Liminf} and @{text Limsup}\<close>
 
 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
@@ -171,7 +171,7 @@
       case False
       then have "C \<le> INFIMUM {x. y < X x} X"
         by (intro INF_greatest) auto
-      with `y < C` show ?thesis
+      with \<open>y < C\<close> show ?thesis
         using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
     qed }
   ultimately show ?thesis
@@ -290,7 +290,7 @@
   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   proof (safe intro!: INF_mono)
     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
-      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
 qed
@@ -303,7 +303,7 @@
   have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
   proof (safe intro!: SUP_mono)
     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
-      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
 qed