src/HOL/Fun.thy
changeset 40969 fb2d3ccda5a7
parent 40968 a6fcd305f7dc
child 41229 d797baa3d57c
     1.1 --- a/src/HOL/Fun.thy	Mon Dec 06 09:19:10 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 06 09:25:05 2010 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  theory Fun
     1.6  imports Complete_Lattice
     1.7 +uses ("Tools/type_lifting.ML")
     1.8  begin
     1.9  
    1.10  text{*As a simplification rule, it replaces all function equalities by
    1.11 @@ -126,9 +127,6 @@
    1.12    "map_fun f g h x = g (h (f x))"
    1.13    by (simp add: map_fun_def)
    1.14  
    1.15 -type_lifting map_fun
    1.16 -  by (simp_all add: fun_eq_iff)
    1.17 -
    1.18  
    1.19  subsection {* Injectivity and Bijectivity *}
    1.20  
    1.21 @@ -774,7 +772,9 @@
    1.22    thus False by best
    1.23  qed
    1.24  
    1.25 -subsection {* Proof tool setup *} 
    1.26 +subsection {* Setup *} 
    1.27 +
    1.28 +subsubsection {* Proof tools *}
    1.29  
    1.30  text {* simplifies terms of the form
    1.31    f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
    1.32 @@ -809,7 +809,7 @@
    1.33  *}
    1.34  
    1.35  
    1.36 -subsection {* Code generator setup *}
    1.37 +subsubsection {* Code generator *}
    1.38  
    1.39  types_code
    1.40    "fun"  ("(_ ->/ _)")
    1.41 @@ -840,4 +840,9 @@
    1.42  code_const "id"
    1.43    (Haskell "id")
    1.44  
    1.45 +
    1.46 +subsubsection {* Functorial structure of types *}
    1.47 +
    1.48 +use "Tools/type_lifting.ML"
    1.49 +
    1.50  end