The HOL2P system is an experimental implementation of the logic HOL2P as an extension and modification of John Harrison's HOL-LIGHT (2.20) theorem prover. HOL2P is free open source software. It comes with no warranty of any kind (see the LICENCE file in the distribution), and no guarantee of maintainance. However, please feel free to send any comments or questions to the author.
Last updated by Norbert Voelker on 21th September 2007.