1.1 --- a/src/HOL/Quotient.thy	Fri Feb 19 17:03:53 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Feb 19 17:37:33 2010 +0100
     1.3 @@ -270,7 +270,7 @@
     1.4    In the following theorem R1 can be instantiated with anything,
     1.5    but we know some of the types of the Rep and Abs functions;
     1.6    so by solving Quotient assumptions we can get a unique R1 that
     1.7 -  will be provable; which is why we need to use apply_rsp and
     1.8 +  will be provable; which is why we need to use @{text apply_rsp} and
     1.9    not the primed version *}
    1.10  
    1.11  lemma apply_rsp:
    1.12 @@ -465,7 +465,7 @@
    1.13    using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
    1.14    by metis
    1.15  
    1.16 -section {* Bex1_rel quantifier *}
    1.17 +section {* @{text Bex1_rel} quantifier *}
    1.18  
    1.19  definition
    1.20    Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"