GSYM : thm -> thm
A |- ..(s1 = s2)...(t1 = t2).. -------------------------------- GSYM A |- ..(s2 = s1)...(t2 = t1)..
# ADD;; val it : thm = |- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n)) # GSYM ADD;; val it : thm = |- (!n. n = 0 + n) /\ (!m n. SUC (m + n) = SUC m + n)