DISCH : (term -> thm -> thm)
STRUCTURE
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
HOL  Trindemossen-1