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