changeset 46950 | d0181abdbdac |
parent 46041 | 1e3ff542e83e |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/Partial_Function.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Partial_Function.thy Thu Mar 15 22:08:53 2012 +0100 @@ -6,6 +6,7 @@ theory Partial_Function imports Complete_Partial_Order Option +keywords "partial_function" :: thy_decl uses "Tools/Function/function_lib.ML" "Tools/Function/partial_function.ML"