1\DOC NOT_ELIM
2
3\TYPE {NOT_ELIM : thm -> thm}
4
5\SYNOPSIS
6Transforms {|- ~t} into {|- t ==> F}.
7
8\KEYWORDS
9rule, implication, negation.
10
11\DESCRIBE
12When applied to a theorem {A |- ~t}, the inference rule {NOT_ELIM} returns the
13theorem {A |- t ==> F}.
14{
15      A |- ~t
16   --------------  NOT_ELIM
17    A |- t ==> F
18}
19
20
21\FAILURE
22Fails unless the theorem has a negated conclusion.
23
24\SEEALSO
25Drule.IMP_ELIM, Thm.NOT_INTRO.
26\ENDDOC
27