MP : thm -> thm -> thm
A1 |- t1 ==> t2 A2 |- t1 ---------------------------- MP A1 u A2 |- t2
# let th1 = TAUT `p ==> p \/ q` and th2 = ASSUME `p:bool`;; val th1 : thm = |- p ==> p \/ q val th2 : thm = p |- p # MP th1 th2;; val it : thm = p |- p \/ q