----------------------------------------------------------------------
DISJ2                                                            (Thm)
----------------------------------------------------------------------
DISJ2 : term -> thm -> thm

SYNOPSIS
Introduces a left disjunct into the conclusion of a theorem.

KEYWORDS
rule, disjunction.

DESCRIBE

      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
Thm.DISJ1, Tactic.DISJ1_TAC, Tactic.DISJ2_TAC, Thm.DISJ_CASES.

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