DISJ1

Thm.DISJ1 : thm -> term -> thm

Introduces a right disjunct into the conclusion of a theorem.

       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

See also

Tactic.DISJ1_TAC, Thm.DISJ2, Tactic.DISJ2_TAC, Thm.DISJ_CASES