src/HOL/Lifting.thy
 changeset 61799 4cf66f21b764 parent 61630 608520e0e8e2 child 63092 a949b2a5f51d
```     1.1 --- a/src/HOL/Lifting.thy	Mon Dec 07 10:23:50 2015 +0100
1.2 +++ b/src/HOL/Lifting.thy	Mon Dec 07 10:38:04 2015 +0100
1.3 @@ -55,7 +55,7 @@
1.4    by blast
1.5
1.6  lemma Quotient_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 unfolding Quotient_def
1.10    by blast
1.11
1.12 @@ -318,7 +318,7 @@
1.13
1.14  end
1.15
1.16 -text \<open>Generating transfer rules for a type defined with @{text "typedef"}.\<close>
1.17 +text \<open>Generating transfer rules for a type defined with \<open>typedef\<close>.\<close>
1.18
1.19  context
1.20    fixes Rep Abs A T
1.21 @@ -350,7 +350,7 @@
1.22  end
1.23
1.24  text \<open>Generating the correspondence rule for a constant defined with
1.25 -  @{text "lift_definition"}.\<close>
1.26 +  \<open>lift_definition\<close>.\<close>
1.27
1.28  lemma Quotient_to_transfer:
1.29    assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
```