INSTANTIATE_ALL : instantiation -> thm -> thm
Apply a higher-order instantiation to assumptions and conclusion of a theorem.
The call INSTANTIATE_ALL i t, where i is an instantiation as returned by
term_match, will perform the instantiation indicated by i in the conclusion
of the theorem th: types and terms will be instantiated and the
beta-reductions that are part of higher-order matching will be applied.
- FAILURE CONDITIONS
Never fails on a valid instantiation.
This is not intended for general use. PART_MATCH is generally a more
convenient packaging. The function INSTANTIATE is almost the same but does
not instantiate hypotheses and may fail if type variables or term variables
free in the hypotheses make the instantiation impossible.
- SEE ALSO
INSTANTIATE, INSTANTIATE_ALL, PART_MATCH, term_match.