1\DOC SYM_CONV 2 3\TYPE {SYM_CONV : conv} 4 5\SYNOPSIS 6Interchanges the left and right-hand sides of an equation. 7 8\KEYWORDS 9conversion, symmetry, equality. 10 11\DESCRIBE 12When applied to an equational term {t1 = t2}, the conversion 13{SYM_CONV} returns the theorem: 14{ 15 |- (t1 = t2) = (t2 = t1) 16} 17 18 19\FAILURE 20Fails if applied to a term that is not an equation. 21 22\SEEALSO 23Thm.SYM. 24\ENDDOC 25