Induct_on : term -> tactic
STRUCTURE
SYNOPSIS
Induct on given term.
DESCRIPTION
bossLib.Induct_on is identical to BasicProvers.Induct_on.
SEEALSO
HOL  Kananaskis-10