DISJ1 : thm -> term -> thm

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

DESCRIPTION
       A |- t1
   ---------------  DISJ1 (A |- t1) `t2`
    A |- t1 \/ t2

FAILURE CONDITIONS
Fails unless the term argument is boolean.

EXAMPLE
  # DISJ1 TRUTH `F`;;
  val it : thm = |- T \/ F

SEE ALSO
DISJ1_TAC, DISJ2, DISJ2_TAC, DISJ_CASES.