1\DOC UNDISCH_TAC
2
3\TYPE {UNDISCH_TAC : term -> tactic}
4
5\SYNOPSIS
6Undischarges an assumption and deletes all assumptions that are
7alpha-equivalent to it.
8
9\KEYWORDS
10tactic, discharge.
11
12\DESCRIBE
13Let {a1} to {an} be the assumptions that are alpha-equivalent to {v}, then
14{
15               A ?- t
16   ==============================  UNDISCH_TAC v
17    A - {a1, ..., an} ?- v ==> t
18}
19
20In particular, if {v} is among the assumptions of the goal and no other
21assumption is alpha-equivalent to it, then {UNDISCH_TAC} behaves as the
22opposite of {DISCH_TAC}:
23{
24          A ?- t
25   ====================  UNDISCH_TAC v
26    A - {v} ?- v ==> t
27}
28
29\FAILURE
30{UNDISCH_TAC} fails if no assumption is alpha-equivalent to {v}.
31
32\COMMENTS
33In the typical use {v} is among the assumptions. If only a single
34assumption alpha-equivalent to {v}, but it is different from {v} then the
35action of {UNDISCH_TAC} can be seen as undischarging followed by
36alpha-conversion.
37
38\SEEALSO
39Thm.DISCH, Drule.DISCH_ALL, Tactic.DISCH_TAC, Thm_cont.DISCH_THEN, Drule.NEG_DISCH, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Tactic.STRIP_TAC, Drule.UNDISCH, Drule.UNDISCH_ALL.
40\ENDDOC
41