MP_TAC : thm_tactic
STRUCTURE
SYNOPSIS
Reduces a goal to implication from a known theorem.
DESCRIPTION
When applied to the theorem A' |- s and the goal A ?- t, the tactic MP_TAC reduces the goal to A ?- s ==> t. Unless A' is a subset of A, this is an invalid tactic.
       A ?- t
   ==============  MP_TAC (A' |- s)
    A ?- s ==> t

FAILURE
Never fails.
SEEALSO
HOL  Kananaskis-14