----------------------------------------------------------------------
IMP_ELIM                                                       (Drule)
----------------------------------------------------------------------
IMP_ELIM : (thm -> thm)

SYNOPSIS
Transforms {|- s ==> t} into {|- ~s \/ t}.

KEYWORDS
rule, implication, disjunction, negation.

DESCRIBE
When applied to a theorem {A |- s ==> t}, the inference rule {IMP_ELIM}
returns the theorem {A |- ~s \/ t}.

    A |- s ==> t
   --------------  IMP_ELIM
    A |- ~s \/ t




FAILURE
Fails unless the theorem is implicative.

SEEALSO
Thm.NOT_INTRO, Thm.NOT_ELIM.

----------------------------------------------------------------------