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

DISCH_TAC : tactic

SYNOPSIS

Moves the antecedent of an implicative goal into the assumptions.

DESCRIPTION

    A ?- u ==> v
   ==============  DISCH_TAC
    A u {u} ?- v

Note that DISCH_TAC treats `~u` as `u ==> F`, so will also work when applied to a goal with a negated conclusion.

FAILURE CONDITIONS

DISCH_TAC will fail for goals which are not implications or negations.

USES

Solving goals of the form `u ==> v` by rewriting `v` with `u`, although the use of DISCH_THEN is usually more elegant in such cases.

COMMENTS

If the antecedent already appears in the assumptions, it will be duplicated.