----------------------------------------------------------------------
GEN_ALL                                                     (hol88Lib)
----------------------------------------------------------------------
GEN_ALL : thm -> thm

SYNOPSIS
Generalizes the conclusion of a theorem over its own free variables.

DESCRIBE
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
Drule.GEN_ALL.

----------------------------------------------------------------------