MATCH_MP_TAC : thm_tactic
A' |- !x1...xn. s ==> t
A ?- t' ====================== MATCH_MP_TAC (A' |- !x1...xn. s ==> t) A ?- ?z1...zp. s'
# g `!n:num. n <= n * n`;;
# num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)
# e(MATCH_MP_TAC num_INDUCTION);; val it : goalstack = 1 subgoal (1 total) `0 <= 0 * 0 /\ (!n. n <= n * n ==> SUC n <= SUC n * SUC n)`