| changeset 66364 | fa3247e6ee4b |
| parent 64634 | 5bd30359e46e |
| child 67091 | 1393c2340eec |
--- a/src/HOL/Partial_Function.thy Mon Aug 07 11:21:07 2017 +0200 +++ b/src/HOL/Partial_Function.thy Mon Aug 07 11:21:11 2017 +0200 @@ -5,8 +5,8 @@ section \<open>Partial Function Definitions\<close> theory Partial_Function -imports Complete_Partial_Order Fun_Def_Base Option -keywords "partial_function" :: thy_decl + imports Complete_Partial_Order Option + keywords "partial_function" :: thy_decl begin named_theorems partial_function_mono "monotonicity rules for partial function definitions"