NOT_INTRO : thm -> 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 CONDITIONS

Fails unless the theorem has an implicative conclusion with F as the consequent.

EXAMPLE

  # let th = TAUT `F ==> F`;;
  val th : thm = |- F ==> F

  # NOT_INTRO th;;
  val it : thm = |- ~F

SEE ALSO

EQF_ELIM, EQF_INTRO, NOT_ELIM.