Papers

L. Théry,  Y. Bertot and G. Kahn

Real Theorem Provers Deserve Real User Interfaces

Click here to get the article

L. Théry  

A proof development system for the HOL theorem prover

Click here to get the article

Chol Documentation

Click here to get the documentation for HOL90


Click here to get the documentation for HOL88