MP-TAC : TACTICMP-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Applies MP if a support line is an implication.
As defined for use ETREE-NAT: is a primitive tactic.
If a support line is an implication, planned line follows from the
succedent and the antecedent is provable, applies Modus Ponens. Same
as Pfenning's tactic 209.
TPS documentation homepage