DISCH_ALL : thm -> thm

SYNOPSIS
Discharges all hypotheses of a theorem.

DESCRIPTION
         A1, ..., An |- t
   ----------------------------  DISCH_ALL
    |- A1 ==> ... ==> An ==> t

FAILURE CONDITIONS
DISCH_ALL will not fail if there are no hypotheses to discharge, it will simply return the theorem unchanged.

EXAMPLE
  # end_itlist CONJ (map ASSUME [`p:bool`; `q:bool`; `r:bool`]);;
  val it : thm = p, q, r |- p /\ q /\ r

  # DISCH_ALL it;;
  val it : thm = |- r ==> q ==> p ==> p /\ q /\ r

COMMENTS
Users should not rely on the hypotheses being discharged in any particular order. Two or more alpha-convertible hypotheses will be discharged by a single implication; users should not rely on which hypothesis appears in the implication.

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