equal
deleted
inserted
replaced
32 ((bstring * term) * theory attribute list) list -> |
32 ((bstring * term) * theory attribute list) list -> |
33 thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
33 thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
34 val add_inductive_x: string list * string -> ((bstring * string) * theory attribute list) list |
34 val add_inductive_x: string list * string -> ((bstring * string) * theory attribute list) list |
35 -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
35 -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
36 val add_inductive: string list * string -> |
36 val add_inductive: string list * string -> |
37 ((bstring * string) * Args.src list) list -> |
37 ((bstring * string) * Attrib.src list) list -> |
38 (thmref * Args.src list) list * (thmref * Args.src list) list * |
38 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list * |
39 (thmref * Args.src list) list * (thmref * Args.src list) list -> |
39 (thmref * Attrib.src list) list * (thmref * Attrib.src list) list -> |
40 theory -> theory * inductive_result |
40 theory -> theory * inductive_result |
41 end; |
41 end; |
42 |
42 |
43 |
43 |
44 (*Declares functions to add fixedpoint/constructor defs to a theory. |
44 (*Declares functions to add fixedpoint/constructor defs to a theory. |