MP_TAC
Tactic.MP_TAC : thm_tactic
Reduces a goal to implication from a known theorem.
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.