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

SYNOPSIS
Applies the first tactic in a tactic list which succeeds.

KEYWORDS
tactical.

DESCRIBE
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
Tactical.EVERY, Tactical.ORELSE.

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