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