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.