INST_TY_TERM
Drule.INST_TY_TERM :
(term,term)subst * (hol_type,hol_type)subst -> thm -> thm
Instantiates terms and types of a theorem.
INST_TY_TERM instantiates types in a theorem, in the same way
INST_TYPE does. Then it instantiates some or all of the free variables
in the resulting theorem, in the same way as INST.
Comments
Because the types are instantiated first, the terms (redexes as well as
residues) in the term substitution must contain the substituted types,
not the original ones. Use norm_subst to achieve this.
Failure
INST_TY_TERM fails under the same conditions as either INST or
INST_TYPE fail.
See also
Thm.INST, Thm.INST_TYPE,
Drule.ISPEC, Thm.SPEC,
Drule.SUBS, Thm.SUBST,
Term.norm_subst,
Drule.INST_TT_HYPS