src/HOL/Library/Extended_Real.thy

 begin
 
 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>
 
 lemma continuous_at_left_imp_sup_continuous:
   fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}"

 lemma inverse_ereal_tendsto_pos: 
   fixes x :: ereal assumes "0 < x"
   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
              intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
 qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)