src/HOL/ex/Transfer_Int_Nat.thy
changeset 61933 cf58b5b794b2
parent 61649 268d88ec9087
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 26 15:44:14 2015 +0100
     1.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 26 15:59:27 2015 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    apply simp_all
     1.5    done
     1.6  
     1.7 -text \<open>For derived operations, we can use the @{text "transfer_prover"}
     1.8 +text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
     1.9    method to help generate transfer rules.\<close>
    1.10  
    1.11  lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
    1.12 @@ -159,8 +159,8 @@
    1.13  apply fact
    1.14  done
    1.15  
    1.16 -text \<open>The @{text "fixing"} option prevents generalization over the free
    1.17 -  variable @{text "n"}, allowing the local transfer rule to be used.\<close>
    1.18 +text \<open>The \<open>fixing\<close> option prevents generalization over the free
    1.19 +  variable \<open>n\<close>, allowing the local transfer rule to be used.\<close>
    1.20  
    1.21  lemma
    1.22    assumes [transfer_rule]: "ZN x n"
    1.23 @@ -185,7 +185,7 @@
    1.24  apply fact
    1.25  done
    1.26  
    1.27 -text \<open>Quantifiers over higher types (e.g. @{text "nat list"}) are
    1.28 +text \<open>Quantifiers over higher types (e.g. \<open>nat list\<close>) are
    1.29    transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close>
    1.30  
    1.31  lemma