src/HOL/Fun.thy
changeset 40969 fb2d3ccda5a7
parent 40968 a6fcd305f7dc
child 41229 d797baa3d57c
--- a/src/HOL/Fun.thy	Mon Dec 06 09:19:10 2010 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 06 09:25:05 2010 +0100
@@ -7,6 +7,7 @@
 
 theory Fun
 imports Complete_Lattice
+uses ("Tools/type_lifting.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
@@ -126,9 +127,6 @@
   "map_fun f g h x = g (h (f x))"
   by (simp add: map_fun_def)
 
-type_lifting map_fun
-  by (simp_all add: fun_eq_iff)
-
 
 subsection {* Injectivity and Bijectivity *}
 
@@ -774,7 +772,9 @@
   thus False by best
 qed
 
-subsection {* Proof tool setup *} 
+subsection {* Setup *} 
+
+subsubsection {* Proof tools *}
 
 text {* simplifies terms of the form
   f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
@@ -809,7 +809,7 @@
 *}
 
 
-subsection {* Code generator setup *}
+subsubsection {* Code generator *}
 
 types_code
   "fun"  ("(_ ->/ _)")
@@ -840,4 +840,9 @@
 code_const "id"
   (Haskell "id")
 
+
+subsubsection {* Functorial structure of types *}
+
+use "Tools/type_lifting.ML"
+
 end