DISCH
Thm.DISCH : (term -> thm -> thm)
Discharges an assumption.
A |- t
-------------------- DISCH u
A - {u} |- u ==> t
Failure
DISCH will fail if u is not boolean.
Comments
The term u need not be a hypothesis. Discharging u will remove all
identical and alpha-equivalent hypotheses.
See also
Drule.DISCH_ALL,
Tactic.DISCH_TAC,
Thm_cont.DISCH_THEN,
Tactic.FILTER_DISCH_TAC,
Tactic.FILTER_DISCH_THEN,
Drule.NEG_DISCH,
Tactic.STRIP_TAC,
Drule.UNDISCH,
Drule.UNDISCH_ALL,
Tactic.UNDISCH_TAC