inst_goal : instantiation -> goal -> goal
- SYNOPSIS
-
Apply higher-order instantiation to a goal.
- DESCRIPTION
-
The call inst_goal i g where i is an instantiation (as returned by
term_match for example), will perform the instantiation indicated by i in
both assumptions and conclusion of the goal g.
- FAILURE CONDITIONS
-
Should never fail on a valid instantiation.
- COMMENTS
-
Probably only of specialist interest to those writing tactics from scratch.
- SEE ALSO
-
compose_insts, instantiate, INSTANTIATE, INSTANTIATE_ALL,
PART_MATCH, term_match.