src/HOL/Fun.thy
changeset 32554 4ccd84fb19d3
parent 32337 7887cb2848bb
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 10 14:07:58 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 10 15:23:07 2009 +0200
     1.3 @@ -7,6 +7,7 @@
     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 @@ -568,6 +569,16 @@
    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