GENL : term list -> thm -> thm
Generalizes zero or more variables in the conclusion of a theorem.
When applied to a term list [x1;...;xn] and a theorem A |- t, the inference
rule GENL returns the theorem A |- !x1...xn. t, provided none of the
variables xi are free in any of the assumptions. It is not necessary that
any or all of the xi should be free in t.
A |- t
------------------ GENL `[x1;...;xn]` [where no xi is free in A]
A |- !x1...xn. t
- FAILURE CONDITIONS
Fails unless all the terms in the list are variables, none of which are
free in the assumption list.
# SPEC `m + p:num` ADD_SYM;;
val it : thm = |- !n. (m + p) + n = n + m + p
# GENL [`m:num`; `p:num`] it;;
val it : thm = |- !m p n. (m + p) + n = n + m + p
- SEE ALSO
GEN, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, SPEC_TAC.