GENL : term list -> thm -> thm

- STRUCTURE
- SYNOPSIS
- Generalizes zero or more variables in the conclusion of a theorem.
- DESCRIPTION
- When applied to a term list [x1,...,xn] and a theorem A |- t, the inference rule GENL returns the theorem A |- !x1...xn. t, provided none of the variables xi are free in any of the assumptions. It is not necessary that any or all of the xi should be free in t.
A |- t ------------------ GENL [x1,...,xn] [where no xi is free in A] A |- !x1...xn. t

- FAILURE
- Fails unless all the terms in the list are variables, none of which are free in the assumption list.
- SEEALSO

HOL Kananaskis-14