----------------------------------------------------------------------
prim_irule                                                    (Tactic)
----------------------------------------------------------------------
prim_irule : thm_tactic

SYNOPSIS
For a goal which is an instance of the conclusion of the supplied theorem,
replace the goal by the instantiated hypotheses of the supplied theorem.

KEYWORDS
tactic.

DESCRIBE
When given a theorem {th = A' |- t} and a goal {A ?- t'}
where {t} can be matched to {t'} by instantiating free variables,
including appropriate type instantiation,
{prim_irule} replaces the goal by new subgoals which are the hypotheses
{A'}, instantiated

The order of the new subgoals corresponds to the order in which
{hyp th} returns the hypotheses {A'}

FAILURE
Fails unless the theorem has a conclusion which is instantiable to match that
of the goal.

COMMENTS
{irule} also pre-processes the supplied theorem, which will normally be useful

{prim_irule} differs from {MATCH_ACCEPT_TAC} in that hypotheses of the supplied
theorem may also be substituted, and will appear as new subgoals

SEEALSO
Tactic.irule, Tactic.MATCH_ACCEPT_TAC, Tactic.ACCEPT_TAC.

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