DISCARD_TAC : thm_tactic
STRUCTURE
Tactic
SYNOPSIS
Discards a theorem already present in a goal’s assumptions.
DESCRIPTION
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
POP_ASSUM, POP_ASSUM_LIST
HOL  Kananaskis-14