PSPEC_PAIR : thm -> term * thm

- STRUCTURE
- SYNOPSIS
- Specializes the conclusion of a theorem, returning the chosen variant.
- DESCRIPTION
- When applied to a theorem A |- !p. t, the inference rule PSPEC_PAIR returns the term q' and the theorem A |- t[q'/p], where q' is a variant of p chosen to avoid free variable capture.
A |- !p. t -------------- PSPEC_PAIR A |- t[q'/q]

- FAILURE
- Fails unless the theorem’s conclusion is a paired universal quantification.
- COMMENTS
- This rule is very similar to plain PSPEC, except that it returns the variant chosen, which may be useful information under some circumstances.
- SEEALSO

HOL Kananaskis-14