1\DOC PGEN 2 3\TYPE {PGEN : (term -> thm -> thm)} 4 5\KEYWORDS 6rule, quantifier, universal. 7 8\LIBRARY 9pair 10 11\SYNOPSIS 12Generalizes the conclusion of a theorem. 13 14\DESCRIBE 15When applied to a paired structure of variables {p} and a theorem {A |- t}, 16the inference rule {PGEN} returns the theorem {A |- !p. t}, provided that 17no variable in {p} occurs free in the assumptions {A}. 18There is no compulsion that the variables of {p} should be free in {t}. 19{ 20 A |- t 21 ------------ PGEN "p" [where p does not occur free in A] 22 A |- !p. t 23} 24 25 26\FAILURE 27Fails if {p} is not a paired structure of variables, 28of if any variable in {p} is free in the assumptions. 29 30\SEEALSO 31Thm.GEN, PairRules.PGENL, PairRules.PGEN_TAC, PairRules.PSPEC, 32PairRules.PSPECL, PairRules.PSPEC_ALL, PairRules.PSPEC_TAC. 33 34\ENDDOC 35