GEN : term -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Generalizes the conclusion of a theorem.
DESCRIPTION
When applied to a term x and a theorem A |- t, the inference rule GEN returns the theorem A |- !x. t, provided x is a variable not free in any of the assumptions. There is no compulsion that x should be free in t. 
      A |- t
   ------------  GEN x                [where x is not free in A]
    A |- !x. t

FAILURE
Fails if x is not a variable, or if it is free in any of the assumptions.
EXAMPLE
The following example shows how the above side-condition prevents the derivation of the theorem x=T |- !x. x=T, which is clearly invalid. 
   - show_types := true;
   > val it = () : unit

   - val t = ASSUME (Term `x=T`);
   > val t =  [.] |- (x :bool) = T : thm

   - try (GEN (Term `x:bool`)) t;
   Exception raised at Thm.GEN:
   variable occurs free in hypotheses
   ! Uncaught exception:
   ! HOL_ERR

SEEALSO
GENL, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, SPEC_TAC, GEN_ASSUM, GEN_IMP, GEN_EQ
HOL  Kananaskis-13