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