src/HOL/Fun.thy
changeset 33318 ddd97d9dfbfb
parent 33057 764547b68538
child 34101 d689f0b33047
     1.1 --- a/src/HOL/Fun.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  theory Fun
     1.6  imports Complete_Lattice
     1.7 -uses ("Tools/transfer.ML")
     1.8  begin
     1.9  
    1.10  text{*As a simplification rule, it replaces all function equalities by
    1.11 @@ -604,16 +603,6 @@
    1.12  *}
    1.13  
    1.14  
    1.15 -subsection {* Generic transfer procedure *}
    1.16 -
    1.17 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    1.18 -  where "TransferMorphism a B \<longleftrightarrow> True"
    1.19 -
    1.20 -use "Tools/transfer.ML"
    1.21 -
    1.22 -setup Transfer.setup
    1.23 -
    1.24 -
    1.25  subsection {* Code generator setup *}
    1.26  
    1.27  types_code