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