INST : (term * term) list -> thm -> thm
A |- t ----------------------------------- INST_TYPE [t1,x1;...;tn,xn] A[t1,...,tn/x1,...,xn] |- t[t1,...,tn/x1,...,xn]
# let th = SPEC_ALL ADD_SYM;; val th : thm = |- m + n = n + m # INST [`1`,`m:num`; `x:num`,`n:num`] th;; val it : thm = |- 1 + x = x + 1
# let th = SPEC_ALL LE_EXISTS;; val th : thm = |- m <= n <=> (?d. n = m + d) # INST [`d:num`,`m:num`] th;; val it : thm = |- d <= n <=> (?d'. n = d + d')