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"
```