src/HOL/Quotient.thy
changeset 61799 4cf66f21b764
parent 60758 d8d85a8172b5
child 63343 fb5d8a50c641
     1.1 --- a/src/HOL/Quotient.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4    by blast
     1.5  
     1.6  lemma Quotient3_rel:
     1.7 -  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- \<open>orientation does not loop on rewriting\<close>
     1.8 +  "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>
     1.9    using a
    1.10    unfolding Quotient3_def
    1.11    by blast
    1.12 @@ -196,7 +196,7 @@
    1.13    In the following theorem R1 can be instantiated with anything,
    1.14    but we know some of the types of the Rep and Abs functions;
    1.15    so by solving Quotient assumptions we can get a unique R1 that
    1.16 -  will be provable; which is why we need to use @{text apply_rsp} and
    1.17 +  will be provable; which is why we need to use \<open>apply_rsp\<close> and
    1.18    not the primed version\<close>
    1.19  
    1.20  lemma apply_rspQ3:
    1.21 @@ -392,7 +392,7 @@
    1.22    using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
    1.23    by metis
    1.24  
    1.25 -subsection \<open>@{text Bex1_rel} quantifier\<close>
    1.26 +subsection \<open>\<open>Bex1_rel\<close> quantifier\<close>
    1.27  
    1.28  definition
    1.29    Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"