1\DOC INST_TY_TERM
2
3\BLTYPE
4INST_TY_TERM :
5(term,term)subst * (hol_type,hol_type)subst -> thm -> thm
6\ELTYPE
7
8\SYNOPSIS
9Instantiates terms and types of a theorem.
10
11\KEYWORDS
12rule, type, instantiate.
13
14\DESCRIBE
15{INST_TY_TERM} instantiates types in a theorem, in the same way
16{INST_TYPE} does. Then it instantiates some or all of the free
17variables in the resulting theorem, in the same way as {INST}.
18
19\COMMENTS
20Because the types are instantiated first, the terms (redexes as well as
21residues) in the term substitution must contain the substituted types, not the
22original ones. Use {norm_subst} to achieve this.
23
24\FAILURE
25{INST_TY_TERM} fails under the same conditions as either {INST} or
26{INST_TYPE} fail.
27
28\SEEALSO
29Thm.INST, Thm.INST_TYPE, Drule.ISPEC, Thm.SPEC, Drule.SUBS, Thm.SUBST,
30Term.norm_subst, Drule.INST_TT_HYPS
31\ENDDOC
32