DISCH_ALL : thm -> thm
STRUCTURE
SYNOPSIS
Discharges all hypotheses of a theorem.
DESCRIPTION
         A1, ..., An |- t
   ----------------------------  DISCH_ALL
    |- A1 ==> ... ==> An ==> t

FAILURE
DISCH_ALL never fails. If there are no hypotheses to discharge, it will simply return the theorem unchanged.
COMMENTS
Users should not rely on the hypotheses being discharged in any particular order.
SEEALSO
HOL  Kananaskis-13