ISPECL : term list -> thm -> thm
A |- !x1...xn.t ----------------------------- ISPECL [`t1`,...,`tn`] A' |- t[t1,...tn/x1,...,xn]
# ISPECL [`x:num`; `2`] EQ_SYM_EQ;; val it : thm = |- x = 2 <=> 2 = x
# SPECL [`x:num`; `2`] EQ_SYM_EQ;; Exception: Failure "SPECL".