(THENC) : conv -> conv -> conv

SYNOPSIS
Applies two conversions in sequence.

DESCRIPTION
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.

FAILURE CONDITIONS
(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').

EXAMPLE
  # BETA_CONV `(\x. x + 1) 3`;;
  val it : thm = |- (\x. x + 1) 3 = 3 + 1
  # (BETA_CONV THENC NUM_ADD_CONV) `(\x. x + 1) 3`;;
  val it : thm = |- (\x. x + 1) 3 = 4

SEE ALSO
EVERY_CONV, ORELSEC, REPEATC.