GSPEC : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Specializes the conclusion of a theorem with unique variables.
DESCRIPTION
When applied to a theorem A |- !x1...xn. t, where the number of universally quantified variables may be zero, GSPEC returns A |- t[g1/x1]...[gn/xn], where the gi are distinct variable names of the appropriate type, chosen by genvar. 
        A |- !x1...xn. t
   -------------------------  GSPEC
    A |- t[g1/x1]...[gn/xn]

FAILURE
Never fails.
USES
GSPEC is useful in writing derived inference rules which need to specialize theorems while avoiding using any variables that may be present elsewhere.
SEEALSO
GEN, GENL, genvar, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, SPEC_TAC
HOL  Kananaskis-13