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
|
\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
}
\FAILURE
{UNDISCH} will fail on theorems which are not implications.
\EXAMPLE
{
# UNDISCH(TAUT `p /\ q ==> p`);;
val it : thm = p /\ q |- p
}
\SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, STRIP_TAC, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|
