DISCH_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Moves the antecedent of an implicative goal into the assumptions.
- DESCRIPTION
- Note that DISCH_TAC treats ~u as u ==> F, so will also work when applied to a goal with a negated conclusion.
A ?- u ==> v ============== DISCH_TAC A u {u} ?- v

- FAILURE
- DISCH_TAC will fail for goals which are not implications or negations.
- USES
- Solving goals of the form u ==> v by rewriting v with u, although the use of DISCH_THEN is usually more elegant in such cases.
- COMMENTS
- If the antecedent already appears in the assumptions, it will be duplicated.
- SEEALSO

HOL Kananaskis-14