--- a/src/HOL/Library/Extended_Real.thy Tue Nov 10 14:18:41 2015 +0000
+++ b/src/HOL/Library/Extended_Real.thy Tue Nov 10 14:43:29 2015 +0000
@@ -14,7 +14,7 @@
text \<open>
This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
-AFP-entry @{text "Jinja_Thread"} fails, as it does overload certain named from @{theory Complex_Main}.
+AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
\<close>
@@ -3607,7 +3607,7 @@
shows "inverse -- x --> inverse x"
proof (cases x)
case (real r)
- with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+ with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
by (auto intro!: tendsto_inverse)
from real \<open>0 < x\<close> show ?thesis
by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter