Apply the first of the conversions in a given list that succeeds.
DESCRIPTION
FIRST_CONV [c1;...;cn] `t` returns the result of applying to the term `t`
the first conversion ci that succeeds when applied to `t`. The conversions
are tried in the order in which they are given in the list.
FAILURE CONDITIONS
FIRST_CONV [c1;...;cn] `t` fails if all the conversions c1, ..., cn fail
when applied to the term `t`. FIRST_CONV cs `t` also fails if cs is the
empty list.
EXAMPLE
# FIRST_CONV [NUM_ADD_CONV; NUM_MULT_CONV; NUM_EXP_CONV] `12 * 12`;;
val it : thm = |- 12 * 12 = 144