1\DOC DISCH_TAC 2 3\TYPE {DISCH_TAC : tactic} 4 5\SYNOPSIS 6Moves the antecedent of an implicative goal into the assumptions. 7 8\KEYWORDS 9tactic, undischarge, antecedent, implication. 10 11\DESCRIBE 12{ 13 A ?- u ==> v 14 ============== DISCH_TAC 15 A u {u} ?- v 16} 17Note that {DISCH_TAC} treats {~u} as {u ==> F}, so will also work 18when applied to a goal with a negated conclusion. 19 20\FAILURE 21{DISCH_TAC} will fail for goals which are not implications or negations. 22 23\USES 24Solving goals of the form {u ==> v} by rewriting {v} with {u}, although 25the use of {DISCH_THEN} is usually more elegant in such cases. 26 27\COMMENTS 28If the antecedent already appears in the assumptions, it will be duplicated. 29 30\SEEALSO 31Thm.DISCH, Drule.DISCH_ALL, Thm_cont.DISCH_THEN, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Drule.NEG_DISCH, Tactic.STRIP_TAC, Drule.UNDISCH, Drule.UNDISCH_ALL, Tactic.UNDISCH_TAC. 32\ENDDOC 33