PGEN
PairRules.PGEN : (term -> thm -> thm)
Generalizes the conclusion of a theorem.
When applied to a paired structure of variables p and a theorem
A |- t, the inference rule PGEN returns the theorem A |- !p. t,
provided that no variable in p occurs free in the assumptions A.
There is no compulsion that the variables of p should be free in t.
A |- t
------------ PGEN "p" [where p does not occur free in A]
A |- !p. t
Failure
Fails if p is not a paired structure of variables, of if any variable
in p is free in the assumptions.
See also
Thm.GEN, PairRules.PGENL,
PairRules.PGEN_TAC,
PairRules.PSPEC,
PairRules.PSPECL,
PairRules.PSPEC_ALL,
PairRules.PSPEC_TAC