Specialize : term -> thm -> thm
STRUCTURE
SYNOPSIS
Specializes the conclusion of a universal theorem.
DESCRIPTION
When applied to a term u and a theorem A |- !x. t, Specialize returns the theorem A |- t[u/x]. Care is taken to ensure that no variables free in u become bound after this operation.
     A |- !x. t
   --------------  Specialize u
    A |- t[u/x]

FAILURE
Fails if the theorem’s conclusion is not universally quantified, or if x and u have different types.
COMMENTS
Specialize behaves identically to SPEC, but is faster.
SEEALSO
HOL  Trindemossen-1