----------------------------------------------------------------------
FIRST_PROVE                                                 (Tactical)
----------------------------------------------------------------------
FIRST_PROVE : (tactic list -> tactic)

SYNOPSIS
Applies the first tactic in a tactic list which completely proves the goal.

KEYWORDS
tactical.

DESCRIBE
When applied to a list of tactics {[T1;...;Tn]}, and a goal {g}, the tactical
{FIRST_PROVE} tries applying the tactics to the goal until one proves the goal. If the
first tactic which proves the goal is {Tm}, then the effect is the same as just {Tm}.
Thus {FIRST_PROVE} effectively behaves as follows:

   FIRST_PROVE [T1;...;Tn] = (T1 THEN NO_TAC) ORELSE ... ORELSE (Tn THEN NO_TAC)




FAILURE
The application of {FIRST_PROVE} to a tactic list never fails. The resulting
tactic fails iff none of the supplied tactics completely proves the goal by itself,
or if the tactic list is empty.

SEEALSO
Tactical.EVERY, Tactical.ORELSE, Tactical.FIRST.

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