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