----------------------------------------------------------------------
ACCEPT_TAC                                                    (Tactic)
----------------------------------------------------------------------
ACCEPT_TAC : thm_tactic

SYNOPSIS
Solves a goal if supplied with the desired theorem (up to alpha-conversion).

KEYWORDS
tactic.

DESCRIBE
{ACCEPT_TAC} maps a given theorem {th} to a tactic that solves any goal whose
conclusion is alpha-convertible to the conclusion of {th}.

FAILURE
{ACCEPT_TAC th (A,g)} fails if the term {g} is not alpha-convertible to the
conclusion of the supplied theorem {th}.

EXAMPLE
{ACCEPT_TAC} applied to the axiom

   BOOL_CASES_AX = |- !t. (t = T) \/ (t = F)

will solve the goal

   ?- !x. (x = T) \/ (x = F)

but will fail on the goal

   ?- !x. (x = F) \/ (x = T)




USES
Used for completing proofs by supplying an existing theorem, such as an axiom,
or a lemma already proved.

SEEALSO
Tactic.MATCH_ACCEPT_TAC.

----------------------------------------------------------------------