equal
deleted
inserted
replaced
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 -> Nominal_Function_Common.function_result) (* proof continuation *) |
20 * (thm -> 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 open Nominal_Function_Common |
31 |
32 |
32 type qgar = string * (string * typ) list * term list * term list * term |
33 type qgar = string * (string * typ) list * term list * term list * term |
33 |
34 |
34 datatype mutual_part = MutualPart of |
35 datatype mutual_part = MutualPart of |