ISPEC : term -> thm -> thm

SYNOPSIS
Specializes a theorem, with type instantiation if necessary.

DESCRIPTION
This rule specializes a quantified variable as does SPEC; it differs from it in also instantiating the type if needed, both in the conclusion and hypotheses:
     A |- !x:ty.tm
  -----------------------  ISPEC `t:ty'`
   A[ty'/ty] |- tm[t/x]
(where t is free for x in tm, and ty' is an instance of ty).

FAILURE CONDITIONS
ISPEC fails if the input theorem is not universally quantified, or if the type of the given term is not an instance of the type of the quantified variable.

EXAMPLE
  # ISPEC `0` EQ_REFL;;
  val it : thm = |- 0 = 0
Note that the corresponding call to SPEC would fail because of the type mismatch:
  # SPEC `0` EQ_REFL;;
  Exception: Failure "SPEC".

SEE ALSO
INST, INST_TYPE, ISPECL, SPEC, type_match.