NEG_DISCH : term -> thm -> thm
STRUCTURE
SYNOPSIS
Discharges an assumption, transforming |- s ==> F into |- ~s.
DESCRIPTION
When applied to a term s and a theorem A |- t, the inference rule NEG_DISCH returns the theorem A - {s} |- s ==> t, or if t is just F, returns the theorem A - {s} |- ~s.
          A |- F
   --------------------  NEG_DISCH    [special case]
      A - {s} |- ~s

          A |- t
   --------------------  NEG_DISCH    [general case]
    A - {s} |- s ==> t

FAILURE
Fails unless the supplied term has type bool.
SEEALSO
HOL  Kananaskis-13