20 val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list -> |
20 val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list -> |
21 Attrib.src option -> theory -> theory |
21 Attrib.src option -> theory -> theory |
22 * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
22 * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
23 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list -> |
23 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list -> |
24 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
24 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
25 val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list |
25 val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list |
26 -> theory -> theory * {induct_rules: thm} |
26 -> theory -> theory * {induct_rules: thm} |
27 val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list |
27 val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list |
28 -> theory -> theory * {induct_rules: thm} |
28 -> theory -> theory * {induct_rules: thm} |
29 val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool -> local_theory -> Proof.state |
29 val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool -> local_theory -> Proof.state |
30 val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool -> local_theory -> Proof.state |
30 val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool -> local_theory -> Proof.state |