1\DOC GENL
2
3\TYPE {GENL : term list -> thm -> thm}
4
5\SYNOPSIS
6Generalizes zero or more variables in the conclusion of a theorem.
7
8\KEYWORDS
9rule, quantifier, universal.
10
11\DESCRIBE
12When applied to a term list {[x1,...,xn]} and a theorem {A |- t}, the inference
13rule {GENL} returns the theorem {A |- !x1...xn. t}, provided none of the
14variables {xi} are free in any of the assumptions. It is not necessary that
15any or all of the {xi} should be free in {t}.
16{
17         A |- t
18   ------------------  GENL [x1,...,xn]       [where no xi is free in A]
19    A |- !x1...xn. t
20}
21
22
23\FAILURE
24Fails unless all the terms in the list are variables, none of which are
25free in the assumption list.
26
27\SEEALSO
28Thm.GEN, Drule.GEN_ALL, Tactic.GEN_TAC, Thm.SPEC, Drule.SPECL, Drule.SPEC_ALL, Tactic.SPEC_TAC.
29\ENDDOC
30