--- 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
--- 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 -