equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 signature NOMINAL_FUNCTION_MUTUAL = |
11 signature NOMINAL_FUNCTION_MUTUAL = |
12 sig |
12 sig |
13 |
13 |
14 val prepare_nominal_function_mutual : Function_Common.function_config |
14 val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config |
15 -> string (* defname *) |
15 -> string (* defname *) |
16 -> ((string * typ) * mixfix) list |
16 -> ((string * typ) * mixfix) list |
17 -> term list |
17 -> term list |
18 -> local_theory |
18 -> local_theory |
19 -> ((thm (* goalstate *) |
19 -> ((thm (* goalstate *) |
20 * (thm -> Function_Common.function_result) (* proof continuation *) |
20 * (thm -> Nominal_Function_Common.function_result) (* proof continuation *) |
21 ) * local_theory) |
21 ) * local_theory) |
22 |
22 |
23 end |
23 end |
24 |
24 |
25 |
25 |
26 structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = |
26 structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = |
27 struct |
27 struct |
28 |
28 |
29 open Function_Lib |
29 open Function_Lib |
30 open Function_Common |
30 open Nominal_Function_Common |
31 |
31 |
32 type qgar = string * (string * typ) list * term list * term list * term |
32 type qgar = string * (string * typ) list * term list * term list * term |
33 |
33 |
34 datatype mutual_part = MutualPart of |
34 datatype mutual_part = MutualPart of |
35 {i : int, |
35 {i : int, |