SYM_CONV : term -> thm

SYNOPSIS

Interchanges the left and right-hand sides of an equation.

DESCRIPTION

When applied to an equational term t1 = t2, the conversion SYM_CONV returns the theorem:

   |- t1 = t2 <=> t2 = t1

FAILURE CONDITIONS

Fails if applied to a term that is not an equation.

EXAMPLE

  # SYM_CONV `2 = x`;;
  val it : thm = |- 2 = x <=> x = 2

SEE ALSO

SYM.