src/HOL/Partial_Function.thy
changeset 48891 c0eafbd55de3
parent 46950 d0181abdbdac
child 51459 bc3651180a09
     1.1 --- a/src/HOL/Partial_Function.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,11 +7,10 @@
     1.4  theory Partial_Function
     1.5  imports Complete_Partial_Order Option
     1.6  keywords "partial_function" :: thy_decl
     1.7 -uses 
     1.8 -  "Tools/Function/function_lib.ML" 
     1.9 -  "Tools/Function/partial_function.ML" 
    1.10  begin
    1.11  
    1.12 +ML_file "Tools/Function/function_lib.ML"
    1.13 +ML_file "Tools/Function/partial_function.ML"
    1.14  setup Partial_Function.setup
    1.15  
    1.16  subsection {* Axiomatic setup *}