SUBS : thm list -> thm -> thm
A1|-t1=v1 ... An|-tn=vn A|-t --------------------------------------------- SUBS[A1|-t1=v1;...;An|-tn=vn] A1 u ... u An u A |- t[v1,...,vn/t1,...,tn] (A|-t)
# let thm1 = SPEC_ALL ADD_SYM and thm2 = SPEC_ALL(CONJUNCT1 ADD_CLAUSES);; val thm1 : thm = |- m + n = n + m val thm2 : thm = |- 0 + n = n
# SUBS [thm1; thm2] (ASSUME `(n + 0) + (0 + m) = m + n`);; val it : thm = (n + 0) + 0 + m = m + n |- (n + 0) + 0 + m = n + m # SUBS [thm1; thm2] (ASSUME `!n. (n + 0) + (0 + m) = m + n`);; val it : thm = !n. (n + 0) + 0 + m = m + n |- !n. (n + 0) + 0 + m = m + n