GPSPEC : (thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Specializes the conclusion of a theorem with unique pairs.
DESCRIPTION
When applied to a theorem A |- !p1...pn. t, where the number of universally quantified variables may be zero, GPSPEC returns A |- t[g1/p1]...[gn/pn], where the gi is paired structures of the same structure as pi and made up of distinct variables , chosen by genvar. 
        A |- !p1...pn. t
   -------------------------  GPSPEC
    A |- t[g1/p1]...[gn/pn]

FAILURE
Never fails.
USES
GPSPEC is useful in writing derived inference rules which need to specialize theorems while avoiding using any variables that may be present elsewhere.
SEEALSO
GSPEC, PGEN, PGENL, genvar, PGEN_TAC, PSPEC, PSPECL, PSPEC_ALL, PSPEC_TAC, PSPEC_PAIR
HOL  Kananaskis-13