GEN_ALL
Drule.GEN_ALL : thm -> thm
Generalizes the conclusion of a theorem over its own free variables.
When applied to a theorem A |- t, the inference rule GEN_ALL returns
the theorem A |- !x1...xn. t, where the xi are all the variables, if
any, which are free in t but not in the assumptions.
A |- t
------------------ GEN_ALL
A |- !x1...xn. t
Failure
Never fails.
Comments
Sometimes people write code that depends on the order of the quantification. They shouldn't.
See also
Thm.GEN, Thm.GENL, Thm.SPEC,
Drule.SPECL, Drule.SPEC_ALL,
Tactic.SPEC_TAC