src/HOL/Fun.thy
changeset 41505 6d19301074cf
parent 41229 d797baa3d57c
child 41657 89451110ba8e
     1.1 --- a/src/HOL/Fun.thy	Mon Jan 10 22:03:24 2011 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Jan 11 14:12:37 2011 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Fun
     1.6  imports Complete_Lattice
     1.7 -uses ("Tools/type_lifting.ML")
     1.8 +uses ("Tools/enriched_type.ML")
     1.9  begin
    1.10  
    1.11  text{*As a simplification rule, it replaces all function equalities by
    1.12 @@ -843,6 +843,6 @@
    1.13  
    1.14  subsubsection {* Functorial structure of types *}
    1.15  
    1.16 -use "Tools/type_lifting.ML"
    1.17 +use "Tools/enriched_type.ML"
    1.18  
    1.19  end