src/HOL/Partial_Function.thy
changeset 55085 0e8e4dc55866
parent 54630 9061af4d5ebc
child 57959 1bfed12a7646
     1.1 --- a/src/HOL/Partial_Function.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Partial_Function.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -5,11 +5,10 @@
     1.4  header {* Partial Function Definitions *}
     1.5  
     1.6  theory Partial_Function
     1.7 -imports Complete_Partial_Order Option
     1.8 +imports Complete_Partial_Order Fun_Def_Base Option
     1.9  keywords "partial_function" :: thy_decl
    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