DISCH_ALL
Drule.DISCH_ALL : thm -> thm
Discharges all hypotheses of a theorem.
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.
See also
Thm.DISCH, Tactic.DISCH_TAC,
Thm_cont.DISCH_THEN,
Drule.NEG_DISCH,
Tactic.FILTER_DISCH_TAC,
Tactic.FILTER_DISCH_THEN,
Tactic.STRIP_TAC,
Drule.UNDISCH,
Drule.UNDISCH_ALL,
Tactic.UNDISCH_TAC