src/HOL/ex/Transfer_Int_Nat.thy
changeset 53013 3fbcfa911863
parent 52360 ac7ac2b242a2
child 55938 f20d1db5aa3c
     1.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Using the transfer method between nat and int *}
     1.5  
     1.6  theory Transfer_Int_Nat
     1.7 -imports GCD "~~/src/HOL/Library/Quotient_List"
     1.8 +imports GCD
     1.9  begin
    1.10  
    1.11  subsection {* Correspondence relation *}
    1.12 @@ -20,6 +20,10 @@
    1.13  
    1.14  subsection {* Transfer rules *}
    1.15  
    1.16 +context
    1.17 +begin
    1.18 +interpretation lifting_syntax .
    1.19 +
    1.20  lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
    1.21    unfolding ZN_def bi_unique_def by simp
    1.22  
    1.23 @@ -115,6 +119,8 @@
    1.24  lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
    1.25    unfolding listsum_def [abs_def] by transfer_prover
    1.26  
    1.27 +end
    1.28 +
    1.29  subsection {* Transfer examples *}
    1.30  
    1.31  lemma