DISJ2

Thm.DISJ2 : term -> thm -> thm

Introduces a left disjunct into the conclusion of a theorem.

      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

See also

Thm.DISJ1, Tactic.DISJ1_TAC, Tactic.DISJ2_TAC, Thm.DISJ_CASES