ISPECL : term list -> thm -> thm
Specializes a theorem zero or more times, with type instantiation if necessary.
ISPECL is an iterative version of ISPEC
(where ti is free for xi in tm) in which A' results from
applying all the corresponding type instantiations to the assumption list A.
A |- !x1...xn.t
----------------------------- ISPECL [`t1`,...,`tn`]
A' |- t[t1,...tn/x1,...,xn]
- FAILURE CONDITIONS
ISPECL fails if the list of terms is longer than the number of
quantified variables in the term, or if the type instantiation fails.
Note that the corresponding call to SPECL would fail because of the
# ISPECL [`x:num`; `2`] EQ_SYM_EQ;;
val it : thm = |- x = 2 <=> 2 = x
# SPECL [`x:num`; `2`] EQ_SYM_EQ;;
Exception: Failure "SPECL".
- SEE ALSO
INST_TYPE, INST, ISPEC, SPEC, SPECL, type_match.