IMP_ELIM : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Transforms |- s ==> t into |- ~s \/ t.
DESCRIPTION
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
NOT_INTRO, NOT_ELIM
HOL  Trindemossen-1