FIRST : tactic list -> tactic
Applies the first tactic in a tactic list that succeeds.
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 CONDITIONS
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.
- SEE ALSO