/usr/share/hol88-2.02.19940316/help/ENTRIES/UNDISCH.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 32 | \DOC UNDISCH
\TYPE {UNDISCH : (thm -> thm)}
\SYNOPSIS
Undischarges the antecedent of an implicative theorem.
\KEYWORDS
rule, undischarge, antecedent.
\DESCRIBE
{
A |- t1 ==> t2
---------------- UNDISCH
A, t1 |- t2
}
\noindent Note that {UNDISCH} treats {"~u"} as {"u ==> F"}.
\FAILURE
{UNDISCH} will fail on theorems which are not implications or negations.
\COMMENTS
If the antecedent already appears in the hypotheses, it will not be duplicated.
However, unlike {DISCH},
if the antecedent is alpha-equivalent to one of the hypotheses,
it will still be added to the hypotheses.
\SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, FILTER_DISCH_THEN,
NEG_DISCH, STRIP_TAC, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|