prim_irule : thm_tactic

- STRUCTURE
- 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

HOL Kananaskis-14