1\DOC DISCARD_TAC 2 3\TYPE {DISCARD_TAC : thm_tactic} 4 5\SYNOPSIS 6Discards a theorem already present in a goal's assumptions. 7 8\KEYWORDS 9tactic. 10 11\DESCRIBE 12When applied to a theorem {A' |- s} and a goal, {DISCARD_TAC} 13checks that {s} is simply {T} (true), or already exists (up 14to alpha-conversion) in the assumption list of the goal. In 15either case, the tactic has no effect. Otherwise, it fails. 16{ 17 A ?- t 18 ======== DISCARD_TAC (A' |- s) 19 A ?- t 20} 21 22 23\FAILURE 24Fails if the above conditions are not met, i.e. the theorem's conclusion 25is not {T} or already in the assumption list (up to alpha-conversion). 26 27\SEEALSO 28Tactical.POP_ASSUM, Tactical.POP_ASSUM_LIST. 29\ENDDOC 30