PROVE_TAC : thm list -> tactic
STRUCTURE
SYNOPSIS
Solve a goal with use of hypotheses and supplied lemmas.
DESCRIPTION
An invocation PROVE_TAC thl attempts to solve the goal it is applied to by executing a proof procedure that is semi-complete for pure first order logic. The assumptions of the goal and the theorems in thl are used. The procedure makes special provision for handling polymorphic and higher-order values (lambda terms). It also handles conditional expressions.
FAILURE
PROVE_TAC fails if it searches to a depth equal to the contents of the reference variable mesonLib.max_depth (set to 30 by default, but changeable by the user) without finding a proof.
COMMENTS
PROVE_TAC can only progress the goal to a successful proof of the goal or not at all. In this respect it differs from tactics such as simplification and rewriting. Its ability to solve existential goals and to make effective use of transitivity theorems make it a particularly powerful tactic.
SEEALSO
HOL  Kananaskis-13