/usr/share/hol88-2.02.19940316/help/ENTRIES/ISPEC.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 | \DOC ISPEC
\TYPE {ISPEC : (term -> thm -> thm)}
\SYNOPSIS
Specializes a theorem, with type instantiation if necessary.
\KEYWORDS
rule, type.
\DESCRIBE
This rule specializes a quantified variable as does {SPEC}; it differs
from it in also instantiating the type if needed:
{
A |- !x:ty.tm
----------------------- ISPEC "t:ty'"
A |- tm[t/x]
}
\noindent (where {t} is free for {x} in {tm}, and {ty'} is an instance
of {ty}).
\FAILURE
{ISPEC} fails if the input theorem is not universally quantified, if
the type of the given term is not an instance of the type of the
quantified variable, or if the type variable is free in the
assumptions.
\SEEALSO
INST_TY_TERM, INST_TYPE, ISPECL, SPEC, match.
\ENDDOC
|