changeset 55085 | 0e8e4dc55866 |
parent 54630 | 9061af4d5ebc |
child 57959 | 1bfed12a7646 |
--- a/src/HOL/Partial_Function.thy Mon Jan 20 20:42:43 2014 +0100 +++ b/src/HOL/Partial_Function.thy Mon Jan 20 21:32:41 2014 +0100 @@ -5,11 +5,10 @@ header {* Partial Function Definitions *} theory Partial_Function -imports Complete_Partial_Order Option +imports Complete_Partial_Order Fun_Def_Base Option keywords "partial_function" :: thy_decl begin -ML_file "Tools/Function/function_lib.ML" ML_file "Tools/Function/partial_function.ML" setup Partial_Function.setup