# HG changeset patch
# User haftmann
# Date 1291623905 -3600
# Node ID fb2d3ccda5a785e275c4233ae16e897d116e946d
# Parent  a6fcd305f7dcc79afccd55d4971359021a902937
moved bootstrap of type_lifting to Fun

diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Mon Dec 06 09:19:10 2010 +0100
+++ b/src/HOL/Datatype.thy	Mon Dec 06 09:25:05 2010 +0100
@@ -13,6 +13,12 @@
   ("Tools/Datatype/datatype_realizer.ML")
 begin
 
+subsection {* Prelude: lifting over function space *}
+
+type_lifting map_fun
+  by (simp_all add: fun_eq_iff)
+
+
 subsection {* The datatype universe *}
 
 typedef (Node)
diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/Fun.thy
--- 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
diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Dec 06 09:19:10 2010 +0100
+++ b/src/HOL/HOL.thy	Mon Dec 06 09:25:05 2010 +0100
@@ -32,7 +32,6 @@
   "Tools/async_manager.ML"
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
-  ("Tools/type_lifting.ML")
   "~~/src/Tools/subtyping.ML"
 begin
 
@@ -714,7 +713,6 @@
   and [Pure.elim?] = iffD1 iffD2 impE
 
 use "Tools/hologic.ML"
-use "Tools/type_lifting.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}
diff -r a6fcd305f7dc -r fb2d3ccda5a7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Dec 06 09:19:10 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 06 09:25:05 2010 +0100
@@ -147,7 +147,6 @@
   $(SRC)/Tools/solve_direct.ML \
   $(SRC)/Tools/value.ML \
   HOL.thy \
-  Tools/type_lifting.ML \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
   Tools/simpdata.ML
@@ -243,6 +242,7 @@
   Tools/split_rule.ML \
   Tools/try.ML \
   Tools/typedef.ML \
+  Tools/type_lifting.ML \
   Transitive_Closure.thy \
   Typedef.thy \
   Wellfounded.thy