Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

MP_TAC : thm_tactic

SYNOPSIS

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.

SEE ALSO

MATCH_MP_TAC, MP, UNDISCH_TAC.