29 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list -> |
29 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list -> |
30 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
30 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
31 val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list -> |
31 val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list -> |
32 simpset * thm list -> theory -> |
32 simpset * thm list -> theory -> |
33 theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
33 theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
34 val defer_recdef: xstring -> string list -> (xstring * Args.src list) list |
34 val defer_recdef: xstring -> string list -> (thmref * Args.src list) list |
35 -> theory -> theory * {induct_rules: thm} |
35 -> theory -> theory * {induct_rules: thm} |
36 val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list |
36 val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list |
37 -> theory -> theory * {induct_rules: thm} |
37 -> theory -> theory * {induct_rules: thm} |
38 val recdef_tc: bstring * Args.src list -> xstring -> int option |
38 val recdef_tc: bstring * Args.src list -> xstring -> int option |
39 -> bool -> theory -> ProofHistory.T |
39 -> bool -> theory -> ProofHistory.T |