Sciweavers

TPHOL
1992
IEEE
14 years 3 months ago
The HOL Logic Extended with Quantification over Type Variables
The HOL system is an LCF-style mechanized proof-assistant for conducting proofs in higher order logic. This paper discusses a proposal to extend the primitive basis of the logic un...
Thomas F. Melham