TAUT : term -> thm
# TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`;; val it : thm = |- a \/ b ==> c <=> (a ==> c) /\ (b ==> c)
# TAUT `(p ==> q) \/ (q ==> p)`;; val it : thm = |- (p ==> q) \/ (q ==> p)
# TAUT `(x > 2 ==> y > 3) \/ (y < 3 ==> x > 2)`;; val it : thm = |- (x > 2 ==> y > 3) \/ (y < 3 ==> x > 2)