NOT_ELIM : thm -> thm
STRUCTURE
Thm
SYNOPSIS
Transforms |- ~t into |- t ==> F.
DESCRIPTION
When applied to a theorem A |- ~t, the inference rule NOT_ELIM returns the theorem A |- t ==> F. 
      A |- ~t
   --------------  NOT_ELIM
    A |- t ==> F

FAILURE
Fails unless the theorem has a negated conclusion.
SEEALSO
IMP_ELIM, NOT_INTRO
HOL  Trindemossen-1