----------------------------------------------------------------------
DISCARD_TAC                                                   (Tactic)
----------------------------------------------------------------------
DISCARD_TAC : thm_tactic

SYNOPSIS
Discards a theorem already present in a goal’s assumptions.

KEYWORDS
tactic.

DESCRIBE
When applied to a theorem {A' |- s} and a goal, {DISCARD_TAC}
checks that {s} is simply {T} (true), or already exists (up
to alpha-conversion) in the assumption list of the goal. In
either case, the tactic has no effect. Otherwise, it fails.

    A ?- t
   ========  DISCARD_TAC (A' |- s)
    A ?- t




FAILURE
Fails if the above conditions are not met, i.e. the theorem’s conclusion
is not {T} or already in the assumption list (up to alpha-conversion).

SEEALSO
Tactical.POP_ASSUM, Tactical.POP_ASSUM_LIST.

----------------------------------------------------------------------