/usr/share/hol88-2.02.19940316/help/ENTRIES/DISCH.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 | \DOC DISCH
\TYPE {DISCH : (term -> thm -> thm)}
\SYNOPSIS
Discharges an assumption.
\KEYWORDS
rule, discharge, assumption, implication.
\DESCRIBE
{
A |- t
-------------------- DISCH "u"
A - {{u}} |- u ==> t
}
\FAILURE
{DISCH} will fail if {"u"} is not boolean.
\COMMENTS
The term {"u"} need not be a hypothesis. Discharging {"u"} will remove all
identical and alpha-equivalent hypotheses.
\SEEALSO
DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, FILTER_DISCH_THEN,
NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|