ACCEPT_TAC : thm_tactic

- STRUCTURE
- 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 axiomwill solve the goal
BOOL_CASES_AX = |- !t. (t = T) \/ (t = F)

but will fail on the goal?- !x. (x = T) \/ (x = F)

?- !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

HOL Kananaskis-14