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
33
|
\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 any
identical and alpha-equivalent hypotheses.
\EXAMPLE
{
# DISCH `p /\ q` (CONJUNCT1(ASSUME `p /\ q`));;
val it : thm = |- p /\ q ==> p
}
\SEEALSO
DISCH_ALL, DISCH_TAC, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|
