GSPEC

Drule.GSPEC : (thm -> thm)

Specializes the conclusion of a theorem with unique variables.

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.

GSPEC is useful in writing derived inference rules which need to specialize theorems while avoiding using any variables that may be present elsewhere.

See also

Thm.GEN, Thm.GENL, Term.genvar, Drule.GEN_ALL, Tactic.GEN_TAC, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.SPEC_TAC