1\DOC ACCEPT_TAC
2
3\TYPE {ACCEPT_TAC : thm_tactic}
4
5\SYNOPSIS
6Solves a goal if supplied with the desired theorem (up to alpha-conversion).
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12{ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose
13conclusion is alpha-convertible to the conclusion of {th}.
14
15\FAILURE
16{ACCEPT_TAC th (A,g)} fails if the term {g} is not alpha-convertible to the
17conclusion of the supplied theorem {th}.
18
19\EXAMPLE
20{ACCEPT_TAC} applied to the axiom
21{
22   BOOL_CASES_AX = |- !t. (t = T) \/ (t = F)
23}
24will solve the goal
25{
26   ?- !x. (x = T) \/ (x = F)
27}
28but will fail on the goal
29{
30   ?- !x. (x = F) \/ (x = T)
31}
32
33
34\USES
35Used for completing proofs by supplying an existing theorem, such as an axiom,
36or a lemma already proved.
37
38\SEEALSO
39Tactic.MATCH_ACCEPT_TAC.
40\ENDDOC
41