ISPECL : term list -> thm -> thm

SYNOPSIS

Specializes a theorem zero or more times, with type instantiation if necessary.

DESCRIPTION

ISPECL is an iterative version of ISPEC

         A |- !x1...xn.t
   -----------------------------  ISPECL [`t1`,...,`tn`]
    A' |- t[t1,...tn/x1,...,xn]

(where ti is free for xi in tm) in which A' results from applying all the corresponding type instantiations to the assumption list A.

FAILURE CONDITIONS

ISPECL fails if the list of terms is longer than the number of quantified variables in the term, or if the type instantiation fails.

EXAMPLE

  # ISPECL [`x:num`; `2`] EQ_SYM_EQ;;
  val it : thm = |- x = 2 <=> 2 = x

Note that the corresponding call to SPECL would fail because of the type mismatch:

  # SPECL [`x:num`; `2`] EQ_SYM_EQ;;
  Exception: Failure "SPECL".