DISJ_IMP : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Converts a disjunctive theorem to an equivalent implicative theorem.
DESCRIPTION
The left disjunct of a disjunctive theorem becomes the negated antecedent of the newly generated theorem. 
     A |- t1 \/ t2
   -----------------  DISJ_IMP
    A |- ~t1 ==> t2

FAILURE
Fails if the theorem is not a disjunction.
EXAMPLE
Specializing the built-in theorem LESS_CASES gives the theorem: 
   th = |- m < n \/ n <= m
to which DISJ_IMP may be applied: 
   - DISJ_IMP th;
   > val it = |- ~m < n ==> n <= m : thm

SEEALSO
DISJ_CASES
HOL  Kananaskis-11