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

FAILURE
Fails unless the theorem has an implicative conclusion with F as the consequent.
SEEALSO
IMP_ELIM, NOT_ELIM
HOL  Trindemossen-1