changeset 44237 | 2a2040c9d898 |
parent 43329 | 84472e198515 |
child 44239 | 47ecd30e018d |
--- a/src/HOL/Tools/Function/fun.ML Wed Aug 17 13:14:20 2011 +0200 +++ b/src/HOL/Tools/Function/fun.ML Wed Aug 17 15:14:48 2011 +0200 @@ -7,6 +7,7 @@ signature FUNCTION_FUN = sig + val fun_config : Function_Common.function_config val add_fun : (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Function_Common.function_config -> local_theory -> Proof.context