DISJ2 : term -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Introduces a left disjunct into the conclusion of a theorem.
DESCRIPTION
      A |- t2
   ---------------  DISJ2 "t1"
    A |- t1 \/ t2

FAILURE
Fails if the term argument is not boolean.
EXAMPLE
- DISJ2 F TRUTH;
> val it = |- F \/ T : thm

SEEALSO
DISJ1, DISJ1_TAC, DISJ2_TAC, DISJ_CASES
HOL  Kananaskis-14