1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC DISCH_ALL
\TYPE {DISCH_ALL : (thm -> thm)}
\SYNOPSIS
Discharges all hypotheses of a theorem.
\KEYWORDS
rule, discharge, assumption, implication.
\DESCRIBE
{
A1, ..., An |- t
---------------------------- DISCH_ALL
|- A1 ==> ... ==> An ==> t
}
\FAILURE
{DISCH_ALL} will not fail 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. Two or more alpha-convertible hypotheses will be discharged by a
single implication; users should not rely on which hypothesis appears in the
implication.
\SEEALSO
DISCH, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN,
STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|
