NOT_ELIM : thm -> thm
A |- ~t -------------- NOT_ELIM A |- t ==> F
# let th = UNDISCH(TAUT `p ==> ~ ~p`);; val th : thm = p |- ~ ~p # NOT_ELIM th;; val it : thm = p |- ~p ==> F