GEN_ALL : thm -> thm

- STRUCTURE
- SYNOPSIS
- Generalizes the conclusion of a theorem over its own free variables.
- DESCRIPTION
- 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
- Superseded by Drule.GEN_ALL, which, however, may return a different result. That is why GEN_ALL is in hol88Lib. Sometimes people write code that depends on the order of the quantification. They shouldn’t.
- SEEALSO

HOL Kananaskis-14