DISCH_ALL : thm -> thm
STRUCTURE
Drule
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
DISCH, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC
HOL  Kananaskis-14