MATCH_MP : thm -> thm -> thm
A1 |- !x1..xn. t1 ==> t2 A2 |- t1' -------------------------------------- MATCH_MP A1 u A2 |- !xa..xk. t2'
# let ith = ARITH_RULE `!x z:num. x = y ==> (w + z) + x = (w + z) + y`;; val ith : thm = |- !x z. x = y ==> (w + z) + x = (w + z) + y # let th = ASSUME `w:num = z`;; val th : thm = w = z |- w = z # MATCH_MP ith th;; val it : thm = w = z |- !z'. (w + z') + w = (w + z') + z