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