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