/usr/share/hol88-2.02.19940316/help/ENTRIES/INST.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 | \DOC INST
\TYPE {INST : ((term # term) list -> thm -> thm)}
\SYNOPSIS
Instantiates free variables in a theorem.
\KEYWORDS
rule, instantiate.
\DESCRIBE
{INST} is a rule for substituting arbitrary terms for free variables
in a theorem:
{
A |- t
----------------------------- INST [(t1,x1);...;(tn,xn)]
A |- t[t1,...,tn/x1,...,xn]
}
\noindent where the variables {x1, ..., xn} are not free in the
assumptions {A}.
\FAILURE
{INST} fails if a variable being instantiated is free in the
assumptions.
\EXAMPLE
In the following example a theorem is instantiated for a specific term:
{
#CONJUNCT1 ADD_CLAUSES ;;
|- 0 + m = m
#INST [("2 * x","m:num")] (CONJUNCT1 ADD_CLAUSES) ;;
|- 0 + (2 * x) = 2 * x
}
\SEEALSO
INST_TY_TERM, INST_TYPE, ISPEC, ISPECL, SPEC; SPECL, SUBS, subst, SUBST.
\ENDDOC
|