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