CONJ_ASM1_TAC : tactic

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

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

HOL Kananaskis-14