GSPEC : (thm -> thm)
STRUCTURE
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
HOL  Trindemossen-1