FIRST : (tactic list -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Applies the first tactic in a tactic list which succeeds.
DESCRIPTION
When applied to a list of tactics [T1;...;Tn], and a goal g, the tactical FIRST tries applying the tactics to the goal until one succeeds. If the first tactic which succeeds is Tm, then the effect is the same as just Tm. Thus FIRST effectively behaves as follows: 
   FIRST [T1;...;Tn] = T1 ORELSE ... ORELSE Tn

FAILURE
The application of FIRST to a tactic list never fails. The resulting tactic fails iff all the component tactics do when applied to the goal, or if the tactic list is empty.
SEEALSO
EVERY, ORELSE
HOL  Kananaskis-14