changeset 69913 | ca515cf61651 |
parent 69745 | aec42cee2521 |
child 73411 | 1f1366966296 |
--- a/src/HOL/Partial_Function.thy Thu Mar 14 16:35:58 2019 +0100 +++ b/src/HOL/Partial_Function.thy Thu Mar 14 16:55:06 2019 +0100 @@ -6,7 +6,7 @@ theory Partial_Function imports Complete_Partial_Order Option - keywords "partial_function" :: thy_decl + keywords "partial_function" :: thy_defn begin named_theorems partial_function_mono "monotonicity rules for partial function definitions"