DISCH : (term -> thm -> thm)
STRUCTURE
Thm
SYNOPSIS
Discharges an assumption.
DESCRIPTION
       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.
SEEALSO
DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, FILTER_DISCH_THEN, NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC
HOL  Kananaskis-13