UNDISCH_TAC : term -> tactic

- STRUCTURE
- SYNOPSIS
- Undischarges an assumption and deletes all assumptions that are alpha-equivalent to it.
- DESCRIPTION
- Let a1 to an be the assumptions that are alpha-equivalent to v, then
A ?- t ============================== UNDISCH_TAC v A - {a1, ..., an} ?- v ==> t

In particular, if v is among the assumptions of the goal and no other assumption is alpha-equivalent to it, then UNDISCH_TAC behaves as the opposite of DISCH_TAC:

A ?- t ==================== UNDISCH_TAC v A - {v} ?- v ==> t

- FAILURE
- UNDISCH_TAC fails if no assumption is alpha-equivalent to v.
- COMMENTS
- In the typical use v is among the assumptions. If only a single assumption alpha-equivalent to v, but it is different from v then the action of UNDISCH_TAC can be seen as undischarging followed by alpha-conversion.
- SEEALSO

HOL Kananaskis-14