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