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