PGEN : (term -> thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Generalizes the conclusion of a theorem.
- DESCRIPTION
- 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.
- SEEALSO

HOL Kananaskis-14