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.