src/HOL/Quotient.thy

 
 text{*
   In the following theorem R1 can be instantiated with anything,
   but we know some of the types of the Rep and Abs functions;
   so by solving Quotient assumptions we can get a unique R1 that
-  will be provable; which is why we need to use apply_rsp and
+  will be provable; which is why we need to use @{text apply_rsp} and
   not the primed version *}
 
 lemma apply_rsp:
   fixes f g::"'a \<Rightarrow> 'c"
   assumes q: "Quotient R1 Abs1 Rep1"

   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   by metis
 
-section {* Bex1_rel quantifier *}
+section {* @{text Bex1_rel} quantifier *}
 
 definition
   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 where
   "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"