NEG_DISCH
Drule.NEG_DISCH : term -> thm -> thm
Discharges an assumption, transforming |- s ==> F into |- ~s.
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.