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.
SEE ALSO
DISCH
,
DISCH_ALL
,
DISCH_THEN
,
STRIP_TAC
,
UNDISCH
,
UNDISCH_ALL
,
UNDISCH_TAC
.