1\DOC SYM
2
3\TYPE {SYM : thm -> thm}
4
5\SYNOPSIS
6Swaps left-hand and right-hand sides of an equation.
7
8\KEYWORDS
9rule, symmetry, equality.
10
11\DESCRIBE
12When applied to a theorem {A |- t1 = t2}, the inference rule {SYM} returns
13{A |- t2 = t1}.
14{
15    A |- t1 = t2
16   --------------  SYM
17    A |- t2 = t1
18}
19
20
21\FAILURE
22Fails unless the theorem is equational.
23
24\SEEALSO
25Conv.GSYM, Drule.NOT_EQ_SYM, Thm.REFL.
26\ENDDOC
27