INRIA Sophia Antipolis

CHOL distribution


What it is:

CHOL is an attempt to provide a better user-interface for the HOL theorem prover. It has been developed following a general approach for building user-interfaces for theorem provers. Its characteristics are the following:
graphic interface:
Multi fonts and colors are used to display formulas and commands.
structured editing:
The proof of a proposition is presented as the structured editing of the tactic that proves the proposition.
rewriting tool:
A tool has been developed that filters the theorems of the database with respect to the term to rewrite.
separation between the interface and the prover:
The X interface and HOL run as two separate processes.

How to get it:

The interface runs with the following versions of HOL: HOL88(AKCL) and HOL90 (SML/NJ). The compressed tarfile is 6 MBytes and the full interface takes 15 MBytes. For the moment, only the version for SUN4OS4 is directly available by ftp. If you need other architectures, please send me an email.

If you are interested in getting CHOL, click here.

If you only want to have a look at the documentation, click here.

If you have an old version, a tarfile is available to update the sml version for hol90.7

Problems and suggestions

I continue to maintain and develop the interface. So email me any problems, bug reports, or suggestions. Click here for a summary of the messages so far.

CHOL profits from work done on programming environments, in particular the Centaur system, developed in the Croap group at INRIA Sophia Antipolis.
Laurent Théry / INRIA Sophia Antipolis/