1signature Induction =
2sig
3 include Abbrev
4 type thry = TypeBasePure.typeBase
5
6 val mk_induction
7 : thry -> {fconst : term, R : term, SV : term list,
8 pat_TCs_list: (term * term list) list}
9 -> thm
10
11 val recInduct : thm -> tactic
12
13end
14