ISPEC : term -> thm -> thm
Specializes a theorem, with type instantiation if necessary.
This rule specializes a quantified variable as does SPEC; it differs
from it in also instantiating the type if needed, both in the conclusion and
(where t is free for x in tm, and ty' is an instance
A |- !x:ty.tm
----------------------- ISPEC `t:ty'`
A[ty'/ty] |- tm[t/x]
- FAILURE CONDITIONS
ISPEC fails if the input theorem is not universally quantified, or if
the type of the given term is not an instance of the type of the
Note that the corresponding call to SPEC would fail because of the
# ISPEC `0` EQ_REFL;;
val it : thm = |- 0 = 0
# SPEC `0` EQ_REFL;;
Exception: Failure "SPEC".
- SEE ALSO
INST, INST_TYPE, ISPECL, SPEC, type_match.