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