Applies in sequence all the conversions in a given list of conversions.
DESCRIPTION
EVERY_CONV [c1;...;cn] `t` returns the result of applying the conversions
c1, ..., cn in sequence to the term `t`. The conversions are applied in
the order in which they are given in the list. In particular, if ci `ti`
returns |- ti=ti+1 for i from 1 to n, then
EVERY_CONV [c1;...;cn] `t1` returns |- t1=t(n+1). If the supplied list of
conversions is empty, then EVERY_CONV returns the identity conversion. That
is, EVERY_CONV [] `t` returns |- t=t.
FAILURE CONDITIONS
EVERY_CONV [c1;...;cn] `t` fails if any one of the conversions c1, ...,
cn fails when applied in sequence as specified above.
EXAMPLE
# EVERY_CONV [BETA_CONV; NUM_ADD_CONV] `(\x. x + 2) 5`;;
val it : thm = |- (\x. x + 2) 5 = 7