ACCEPT_TAC : thm_tactic
STRUCTURE
Tactic
SYNOPSIS
Solves a goal if supplied with the desired theorem (up to alpha-conversion).
DESCRIPTION
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
MATCH_ACCEPT_TAC
HOL  Trindemossen-1