prim_irule : thm_tactic
STRUCTURE
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.
DESCRIPTION
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
irule, MATCH_ACCEPT_TAC, ACCEPT_TAC
HOL  Kananaskis-13