SPEC_VAR : thm -> term * thm
STRUCTURE
SYNOPSIS
Specializes the conclusion of a theorem, returning the chosen variant.
DESCRIPTION
When applied to a theorem A |- !x. t, the inference rule SPEC_VAR returns the term x' and the theorem A |- t[x'/x], where x' is a variant of x chosen to avoid free variable capture.
     A |- !x. t
   --------------  SPEC_VAR
    A |- t[x'/x]

FAILURE
Fails unless the theorem’s conclusion is universally quantified.
COMMENTS
This rule is very similar to plain SPEC, except that it returns the variant chosen, which may be useful information under some circumstances.
SEEALSO
HOL  Trindemossen-1