INST_TY_TERM :
(term,term)subst * (hol_type,hol_type)subst -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Instantiates terms and types of a theorem.
DESCRIPTION
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.
FAILURE
INST_TY_TERM fails under the same conditions as either INST or INST_TYPE fail.
SEEALSO
INST, INST_TYPE, ISPEC, SPEC, SUBS, SUBST
HOL  Kananaskis-10