----------------------------------------------------------------------
PROVE_TAC                                               (BasicProvers)
----------------------------------------------------------------------
PROVE_TAC : thm list -> tactic

SYNOPSIS
Solve a goal with use of hypotheses and supplied lemmas.

DESCRIBE
{bossLib.PROVE_TAC} is identical to {BasicProvers.PROVE_TAC}.

SEEALSO
bossLib.PROVE_TAC.

----------------------------------------------------------------------