CONJ_ASM2_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming the second, then prove the second conjunct.
- DESCRIPTION
- When applied to a goal A ?- t1 /\ t2, the tactic CONJ_ASM2_TAC reduces it to two subgoals corresponding to the two conjuncts, assuming the first to prove the second.
A ?- t1 /\ t2 ========================== CONJ_ASM2_TAC A u {t2} ?- t1 A ?- t2

- FAILURE
- Fails unless the conclusion of the goal is a conjunction.
- SEEALSO

HOL Kananaskis-14