SYM

Thm.SYM : thm -> thm

Swaps left-hand and right-hand sides of an equation.

When applied to a theorem A |- t1 = t2, the inference rule SYM returns A |- t2 = t1.

    A |- t1 = t2
   --------------  SYM
    A |- t2 = t1

Failure

Fails unless the theorem is equational.

See also

Conv.GSYM, Drule.NOT_EQ_SYM, Thm.REFL, Tacic.SYM_TAC