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