SYM : thm -> thm
STRUCTURE
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
Fails unless the theorem is equational.
SEEALSO
GSYM, NOT_EQ_SYM, REFL
HOL  Kananaskis-13