GEN_ALL : thm -> thm

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 CONDITIONS

Never fails.

EXAMPLE

  # let th = ARITH_RULE `x < y ==> 2 * x + y + 1 < 3 * y`;;
  val th : thm = |- x < y ==> 2 * x + y + 1 < 3 * y

  # GEN_ALL th;;
  val it : thm = |- !x y. x < y ==> 2 * x + y + 1 < 3 * y

SEE ALSO

GEN, GENL, GEN_ALL, SPEC, SPECL, SPEC_ALL, SPEC_TAC.