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