DISCH : term -> thm -> thm

SYNOPSIS
Discharges an assumption.

DESCRIPTION
       A |- t
--------------------  DISCH `u`
 A - {u} |- u ==> t

FAILURE CONDITIONS
DISCH will fail if `u` is not boolean.

COMMENTS
The term `u` need not be a hypothesis. Discharging `u` will remove any identical and alpha-equivalent hypotheses.

EXAMPLE
  # DISCH `p /\ q` (CONJUNCT1(ASSUME `p /\ q`));;
  val it : thm = |- p /\ q ==> p

SEE ALSO
DISCH_ALL, DISCH_TAC, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.