----------------------------------------------------------------------
THENC                                                           (Conv)
----------------------------------------------------------------------
op THENC : (conv -> conv -> conv)

SYNOPSIS
Applies two conversions in sequence.

KEYWORDS
conversional.

DESCRIBE
If the conversion {c1} returns {|- t = t'} when applied to a term
{``t``}, and {c2} returns {|- t' = t''} when applied to {``t'``}, then
the composite conversion {(c1 THENC c2) ``t``} returns {|- t = t''}.
That is, {(c1 THENC c2) ``t``} has the effect of transforming the term
{``t``} first with the conversion {c1} and then with the conversion
{c2}.

{THENC} also handles the possibility that either of its arguments
might return the {UNCHANGED} exception.  If the first conversion
returns {UNCHANGED} when applied to its argument, {THENC} just returns
the result of the second conversion applied to the same initial term.
If the second conversion raises {UNCHANGED} (and the first did not),
then the result will be the theorem returned by the first conversion.
In this way, unnecessary calls to {TRANS} can be avoided.

FAILURE
(This refers to failure other than by raising {UNCHANGED}).
{(c1 THENC c2) ``t``} fails if either the conversion {c1} fails when
applied to {``t``}, or if {c1 ``t``} succeeds and returns {|- t = t'}
but {c2} fails when applied to {``t'``}.  {(c1 THENC c2) ``t``} may
also fail if either of {c1} or {c2} is not, in fact, a conversion
(i.e. a function that maps a term {t} to a theorem {|- t = t'}).

SEEALSO
Conv.UNCHANGED, Conv.EVERY_CONV.

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