IMP_ELIM
Drule.IMP_ELIM : (thm -> thm)
Transforms |- s ==> t into |- ~s \/ t.
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.