--- 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)
--- 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
--- 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 *}
--- 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