# HG changeset patch
# User wenzelm
# Date 1527970475 -7200
# Node ID 46d5a9f428e1b3d0d2fd1d7d6f7d573550dad60e
# Parent  67a4db47e4f6fb3cf2524ff6a41763d0e057e008
more formal comments;

diff -r 67a4db47e4f6 -r 46d5a9f428e1 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sat Jun 02 22:11:09 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sat Jun 02 22:14:35 2018 +0200
@@ -627,9 +627,10 @@
   "real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
   by (cases y) auto
 
-(*To help with inferences like  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
+text \<open>
+  To help with inferences like \<^prop>\<open>a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y\<close>,
   where x and y are real.
-*)
+\<close>
 
 lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
   using ereal_less_eq(3) order.trans by blast
diff -r 67a4db47e4f6 -r 46d5a9f428e1 src/HOL/Library/Lub_Glb.thy
--- a/src/HOL/Library/Lub_Glb.thy	Sat Jun 02 22:11:09 2018 +0200
+++ b/src/HOL/Library/Lub_Glb.thy	Sat Jun 02 22:14:35 2018 +0200
@@ -221,7 +221,7 @@
 
 lemma isLub_mono_imp_LIMSEQ:
   fixes X :: "nat \<Rightarrow> real"
-  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use \<open>range X\<close> *)
   assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   shows "X \<longlonglongrightarrow> u"
 proof -