FILTER_DISCH_THEN : (thm_tactic -> term -> tactic)
STRUCTURE
Tactic
SYNOPSIS
Conditionally gives to a theorem-tactic the antecedent of an implicative goal.
DESCRIPTION
If FILTER_DISCH_THEN’s second argument, a term, does not occur in the antecedent, then FILTER_DISCH_THEN removes the antecedent and then creates a theorem by ASSUMEing it. This new theorem is passed to FILTER_DISCH_THEN’s first argument, which is subsequently expanded. For example, if 
    A ?- t
   ========  f (ASSUME u)
    B ?- v
then 
    A ?- u ==> t
   ==============  FILTER_DISCH_THEN f
       B ?- v
Note that FILTER_DISCH_THEN treats ~u as u ==> F.
FAILURE
FILTER_DISCH_THEN will fail if a term which is identical, or alpha-equivalent to w occurs free in the antecedent. FILTER_DISCH_THEN will also fail if the theorem is an implication or a negation.
COMMENTS
FILTER_DISCH_THEN is most easily understood by first understanding DISCH_THEN.
USES
For preprocessing an antecedent before moving it to the assumptions, or for using antecedents and then throwing them away.
SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC
HOL  Kananaskis-14