PROVE_TAC

BasicProvers.PROVE_TAC : thm list -> tactic

Solve a goal with use of hypotheses and supplied lemmas.

bossLib.PROVE_TAC is identical to BasicProvers.PROVE_TAC.

See also

bossLib.PROVE_TAC