PSPEC : (term -> thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Specializes the conclusion of a theorem.
DESCRIPTION
When applied to a term q and a theorem A |- !p. t, then PSPEC returns the theorem A |- t[q/p]. If necessary, variables will be renamed prior to the specialization to ensure that q is free for p in t, that is, no variables free in q become bound after substitution. 
     A |- !p. t
   --------------  PSPEC "q"
    A |- t[q/p]

FAILURE
Fails if the theorem’s conclusion is not a paired universal quantification, or if p and q have different types.
EXAMPLE
PSPEC specialised paired quantifications. 
   - PSPEC (Term `(1,2)`) (ASSUME (Term`!(x,y). (x + y) = (y + x)`));
   > val it =  [.] |- 1 + 2 = 2 + 1 : thm

PSPEC treats paired structures of variables as variables and preserves structure accordingly. 

   - PSPEC (Term `x:'a#'a`) (ASSUME (Term `!(x:'a,y:'a). (x,y) = (x,y)`));
   > val it =  [.] |- x = x : thm

SEEALSO
SPEC, IPSPEC, PSPECL, PSPEC_ALL, PGEN, PGENL
HOL  Kananaskis-13