(ORELSEC) : conv -> conv -> conv

SYNOPSIS
Applies the first of two conversions that succeeds.

DESCRIPTION
(c1 ORELSEC c2) `t` returns the result of applying the conversion c1 to the term `t` if this succeeds. Otherwise (c1 ORELSEC c2) `t` returns the result of applying the conversion c2 to the term `t`.

FAILURE CONDITIONS
(c1 ORELSEC c2) `t` fails both c1 and c2 fail when applied to `t`.

EXAMPLE
  # (NUM_ADD_CONV ORELSEC NUM_MULT_CONV) `2 + 2`;;
  val it : thm = |- 2 + 2 = 4

  # (NUM_ADD_CONV ORELSEC NUM_MULT_CONV) `1 * 1`;;
  val it : thm = |- 1 * 1 = 1

SEE ALSO
FIRST_CONV, THENC.