DISJ1 : thm -> term -> thm
STRUCTURE
Thm
SYNOPSIS
Introduces a right disjunct into the conclusion of a theorem.
DESCRIPTION
       A |- t1
   ---------------  DISJ1 (A |- t1) t2
    A |- t1 \/ t2

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

SEEALSO
DISJ1_TAC, DISJ2, DISJ2_TAC, DISJ_CASES
HOL  Kananaskis-13