recInduct : thm -> tactic
STRUCTURE
BasicProvers
SYNOPSIS
Induct with supplied recursion induction scheme.
DESCRIPTION
bossLib.recInduct
is identical to
Induction.recInduct
.
SEEALSO
recInduct
HOL
Kananaskis-10