NOT_ELIM : thm -> thm
STRUCTURE
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
HOL  Trindemossen-1