Adds a theorem as an antecedent to the conclusion of the goal.
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 CONDITIONS
Never fails.
USES
For moving assumptions into the conclusion of the goal, which often makes it
easier to manipulate via REWRITE_TAC or decompose by ANTS_TAC.