FIRST_CONV : (conv list -> conv)
STRUCTURE
SYNOPSIS
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
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.
SEEALSO
HOL  Kananaskis-8