MATCH_ACCEPT_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Solves a goal which is an instance of the supplied theorem.
- DESCRIPTION
- When given a theorem A' |- t and a goal A ?- t' where t can be matched to t' by instantiating variables which are either free or universally quantified at the outer level, including appropriate type instantiation, MATCH_ACCEPT_TAC completely solves the goal.Unless A' is a subset of A, this is an invalid tactic.
A ?- t' ========= MATCH_ACCEPT_TAC (A' |- t)

- FAILURE
- Fails unless the theorem has a conclusion which is instantiable to match that of the goal.
- EXAMPLE
- The following example shows variable and type instantiation at work. We can use the polymorphic list theorem HD:to solve the goal:
HD = |- !h t. HD(CONS h t) = h

simply by:?- HD [1;2] = 1

MATCH_ACCEPT_TAC HD

- COMMENTS
- prim_irule is similar, with differences in the details
- SEEALSO

HOL Kananaskis-14