src/HOL/Quotient.thy

   using a
   unfolding Quotient3_def
   by blast
 
 lemma Quotient3_rel:
-  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- \<open>orientation does not loop on rewriting\<close>
+  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close>
   using a
   unfolding Quotient3_def
   by blast
 
 lemma Quotient3_refl1: 

 
 text\<open>
   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 @{text apply_rsp} and
+  will be provable; which is why we need to use \<open>apply_rsp\<close> and
   not the primed version\<close>
 
 lemma apply_rspQ3:
   fixes f g::"'a \<Rightarrow> 'c"
   assumes q: "Quotient3 R1 Abs1 Rep1"

   assumes a: "Quotient3 R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
   by metis
 
-subsection \<open>@{text Bex1_rel} quantifier\<close>
+subsection \<open>\<open>Bex1_rel\<close> quantifier\<close>
 
 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)))"