----------------------------------------------------------------------
SPEC                                                             (Thm)
----------------------------------------------------------------------
SPEC : term -> thm -> thm

SYNOPSIS
Specializes the conclusion of a theorem.

KEYWORDS
rule.

DESCRIBE
When applied to a term {u} and a theorem {A |- !x. t}, then {SPEC} returns
the theorem {A |- t[u/x]}. If necessary, variables will be renamed prior
to the specialization to ensure that {u} is free for {x} in {t}, that is,
no variables free in {u} become bound after substitution.

     A |- !x. t
   --------------  SPEC u
    A |- t[u/x]




FAILURE
Fails if the theorem’s conclusion is not universally quantified, or if {x} and
{u} have different types.

EXAMPLE
The following example shows how {SPEC} renames bound variables if necessary,
prior to substitution: a straightforward substitution would result in the
clearly invalid theorem {|- ~y ==> (!y. y ==> ~y)}.

   - let val xv = Term `x:bool`
         and yv = Term `y:bool`
     in
       (GEN xv o DISCH xv o GEN yv o DISCH yv) (ASSUME xv)
     end;
   > val it = |- !x. x ==> !y. y ==> x : thm

   - SPEC (Term `~y`) it;
   > val it = |- ~y ==> !y'. y' ==> ~y : thm




SEEALSO
Drule.ISPEC, Drule.SPECL, Drule.SPEC_ALL, Drule.SPEC_VAR, Thm.GEN,
Thm.GENL, Drule.GEN_ALL.

----------------------------------------------------------------------