equal
deleted
inserted
replaced
20 val add_inductive: bool -> bool -> |
20 val add_inductive: bool -> bool -> |
21 (Name.binding * string option * mixfix) list -> |
21 (Name.binding * string option * mixfix) list -> |
22 (Name.binding * string option * mixfix) list -> |
22 (Name.binding * string option * mixfix) list -> |
23 (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> |
23 (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> |
24 local_theory -> InductivePackage.inductive_result * local_theory |
24 local_theory -> InductivePackage.inductive_result * local_theory |
|
25 val codegen_preproc: theory -> thm list -> thm list |
25 val setup: theory -> theory |
26 val setup: theory -> theory |
26 end; |
27 end; |
27 |
28 |
28 structure InductiveSetPackage: INDUCTIVE_SET_PACKAGE = |
29 structure InductiveSetPackage: INDUCTIVE_SET_PACKAGE = |
29 struct |
30 struct |