PSPECL
PairRules.PSPECL : (term list -> thm -> thm)
Specializes zero or more pairs in the conclusion of a theorem.
When applied to a term list [q1;...;qn] and a theorem
A |- !p1...pn. t, the inference rule SPECL returns the theorem
A |- t[q1/p1]...[qn/pn], where the substitutions are made sequentially
left-to-right in the same way as for PSPEC.
A |- !p1...pn. t
-------------------------- SPECL "[q1;...;qn]"
A |- t[q1/p1]...[qn/pn]
It is permissible for the term-list to be empty, in which case the
application of PSPECL has no effect.
Failure
Fails unless each of the terms is of the same type as that of the appropriate quantified variable in the original theorem. Fails if the list of terms is longer than the number of quantified pairs in the theorem.
See also
Drule.SPECL, PairRules.PGEN,
PairRules.PGENL,
PairRules.PGEN_TAC,
PairRules.PSPEC,
PairRules.PSPEC_ALL,
PairRules.PSPEC_TAC