src/HOL/Nat_Transfer.thy
changeset 47324 ed2bad9b7c6a
parent 47255 30a1692557b0
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Nat_Transfer.thy	Tue Apr 03 20:56:32 2012 +0200
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Tue Apr 03 22:04:50 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  theory Nat_Transfer
     1.6  imports Int
     1.7 -uses ("Tools/transfer.ML")
     1.8 +uses ("Tools/legacy_transfer.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Generic transfer machinery *}
    1.12 @@ -16,9 +16,9 @@
    1.13  lemma transfer_morphismI[intro]: "transfer_morphism f A"
    1.14    by (simp add: transfer_morphism_def)
    1.15  
    1.16 -use "Tools/transfer.ML"
    1.17 +use "Tools/legacy_transfer.ML"
    1.18  
    1.19 -setup Transfer.setup
    1.20 +setup Legacy_Transfer.setup
    1.21  
    1.22  
    1.23  subsection {* Set up transfer from nat to int *}