FIRST_PROVE : (tactic list -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Applies the first tactic in a tactic list which completely proves the goal.
DESCRIPTION
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
EVERY, ORELSE, FIRST
HOL  Kananaskis-14