PROVE_TAC : thm list -> tactic
STRUCTURE
BasicProvers
SYNOPSIS
Solve a goal with use of hypotheses and supplied lemmas.
DESCRIPTION
bossLib.PROVE_TAC
is identical to
BasicProvers.PROVE_TAC
.
SEEALSO
PROVE_TAC
HOL
Kananaskis-14