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"