Thm_cont.UNDISCH_THEN : term -> thm_tactic -> tactic
STRUCTURE
Thm_cont
SYNOPSIS
Discharges the assumption given and passes it to a theorem-tactic.
DESCRIPTION
UNDISCH_THEN finds the first assumption equal to the term given, removes it from the assumption list, ASSUMEs it, passes it to the theorem-tactic and then applies the consequent tactic. Thus: 
   UNDISCH_THEN t f ([a1,... ai, t, aj, ... an], goal) =
     f (ASSUME t) ([a1,... ai, aj,... an], goal)
For example, if 
    A u {t1} ?- t
   ===============  f (ASSUME t1)
    B u {t1} ?- v
then 
    A u {t1} ?- t
   ===============  UNDISCH_THEN t1 f
       B ?- v

FAILURE
UNDISCH_THEN will fail on goals where the given term is not in the assumption list.
SEEALSO
PAT_ASSUM, DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC
HOL  Kananaskis-10