SYM : thm -> thm

SYNOPSIS
Swaps left-hand and right-hand sides of an equation.

DESCRIPTION
When applied to a theorem A |- t1 = t2, the inference rule SYM returns A |- t2 = t1.
    A |- t1 = t2
   --------------  SYM
    A |- t2 = t1

FAILURE CONDITIONS
Fails unless the theorem is equational.

EXAMPLE
  # NUM_REDUCE_CONV `12 * 12`;;
  val it : thm = |- 12 * 12 = 144

  # SYM it;;
  val it : thm = |- 144 = 12 * 12

COMMENTS
The SYM rule requires the input theorem to be a simple equation, without additional structure such as outer universal quantifiers. To reverse equality signs deeper inside theorems, you may use GSYM instead.

SEE ALSO
GSYM, REFL, TRANS.