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