SPECL : term list -> thm -> thm

SYNOPSIS
Specializes zero or more variables in the conclusion of a theorem.

DESCRIPTION
When applied to a term list [u1;...;un] and a theorem A |- !x1...xn. t, the inference rule SPECL returns the theorem A |- t[u1/x1]...[un/xn], where the substitutions are made sequentially left-to-right in the same way as for SPEC, with the same sort of alpha-conversions applied to t if necessary to ensure that no variables which are free in ui become bound after substitution.
       A |- !x1...xn. t
   --------------------------  SPECL [`u1`;...;`un`]
     A |- t[u1/x1]...[un/xn]
It is permissible for the term-list to be empty, in which case the application of SPECL has no effect.

FAILURE CONDITIONS
Fails unless each of the terms is of the same as that of the appropriate quantified variable in the original theorem.

EXAMPLE
The following is a specialization of a theorem from theory arithmetic.
  # let t = ARITH_RULE `!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)`;;
  val t : thm = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q

  # SPECL [`1`; `2`; `3`; `4`] t;;
  val it : thm = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4

COMMENTS
In order to specialize variables while also instantiating types of polymorphic variables, use ISPECL instead.

SEE ALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPEC_ALL, SPEC_TAC.