SYM_CONV : term -> thm
Interchanges the left and right-hand sides of an equation.
When applied to an equational term
t1 = t2
, the conversion
returns the theorem:
|- t1 = t2 <=> t2 = t1
Fails if applied to a term that is not an equation.
# SYM_CONV `2 = x`;; val it : thm = |- 2 = x <=> x = 2