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

Fails unless the theorem has a negated conclusion.

EXAMPLE

  # let th = UNDISCH(TAUT `p ==> ~ ~p`);;
  val th : thm = p |- ~ ~p

  # NOT_ELIM th;;
  val it : thm = p |- ~p ==> F

SEE ALSO

EQF_ELIM, EQF_INTRO, NOT_INTRO.