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.