equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature CONSTDEFS = |
9 signature CONSTDEFS = |
10 sig |
10 sig |
11 val add_constdefs: (binding * string option) list * |
11 val add_constdefs: (binding * string option) list * |
12 ((binding * string option * mixfix) option * |
12 ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory |
13 (Attrib.binding * string)) list -> theory -> theory |
|
14 val add_constdefs_i: (binding * typ option) list * |
13 val add_constdefs_i: (binding * typ option) list * |
15 ((binding * typ option * mixfix) option * |
14 ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory |
16 ((binding * attribute list) * term)) list -> theory -> theory |
|
17 end; |
15 end; |
18 |
16 |
19 structure Constdefs: CONSTDEFS = |
17 structure Constdefs: CONSTDEFS = |
20 struct |
18 struct |
21 |
19 |