src/HOL/Fun.thy
changeset 48891 c0eafbd55de3
parent 47579 28f6f4ad69bf
child 49739 13aa6d8268ec
     1.1 --- a/src/HOL/Fun.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  theory Fun
     1.5  imports Complete_Lattices
     1.6  keywords "enriched_type" :: thy_goal
     1.7 -uses ("Tools/enriched_type.ML")
     1.8  begin
     1.9  
    1.10  lemma apply_inverse:
    1.11 @@ -801,7 +800,7 @@
    1.12  
    1.13  subsubsection {* Functorial structure of types *}
    1.14  
    1.15 -use "Tools/enriched_type.ML"
    1.16 +ML_file "Tools/enriched_type.ML"
    1.17  
    1.18  enriched_type map_fun: map_fun
    1.19    by (simp_all add: fun_eq_iff)