equal
deleted
inserted
replaced
7 |
7 |
8 signature FUNCTION_FUN = |
8 signature FUNCTION_FUN = |
9 sig |
9 sig |
10 val fun_config : Function_Common.function_config |
10 val fun_config : Function_Common.function_config |
11 val add_fun : (binding * typ option * mixfix) list -> |
11 val add_fun : (binding * typ option * mixfix) list -> |
12 (Attrib.binding * term) list -> Function_Common.function_config -> |
12 Specification.multi_specs -> Function_Common.function_config -> |
13 local_theory -> Proof.context |
13 local_theory -> Proof.context |
14 val add_fun_cmd : (binding * string option * mixfix) list -> |
14 val add_fun_cmd : (binding * string option * mixfix) list -> |
15 (Attrib.binding * string) list -> Function_Common.function_config -> |
15 Specification.multi_specs_cmd -> Function_Common.function_config -> |
16 bool -> local_theory -> Proof.context |
16 bool -> local_theory -> Proof.context |
17 end |
17 end |
18 |
18 |
19 structure Function_Fun : FUNCTION_FUN = |
19 structure Function_Fun : FUNCTION_FUN = |
20 struct |
20 struct |