GPSPEC : (thm -> thm)
STRUCTURE
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
HOL  Kananaskis-13