src/HOL/Fun.thy

 
 header {* Notions about functions *}
 
 theory Fun
 imports Complete_Lattice
+uses ("Tools/transfer.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
   first-order equalities.*}
 lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"

     end
 in proc end
 *}
 
 
+subsection {* Generic transfer procedure *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+  where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
 subsection {* Code generator setup *}
 
 types_code
   "fun"  ("(_ ->/ _)")
 attach (term_of) {*