HOL theorem-proving system / News: Recent posts

We are pleased to announce the release of the latest version of the HOL4 system. Among the many, many, exciting new features are support for another SML implementation (Poly/ML) and new parsing/printing facilities, including extensive support for Unicode characters. Replace ``!x. P x`` with ``∀x. P x`` today!

Our latest version of HOL4, Kananaskis-4 has been released. It includes a number of powerful new features, as well as improved documentation and bug-fixes.

The latest version of HOL4, Kananaskis-3 has been released. For more information on its new features and bug-fixes, see http://hol.sourceforge.net/kananaskis-3.release.html

Kananaskis-1 has been made pretty well unusable because of a time overflow problem in the underlying Moscow ML v2.00. The working version in CVS has been fixed (for downloading from CVS see http://sourceforge.net/cvs/?group_id=31790 for instructions), at least for non-Windows users.

You can also download a new version of Moscow ML from its home-page at
http://www.dina.dk/~sestoft/mosml.html. You will
need to rebuild Moscow ML, and then all of HOL. There will hopefully be a Windows version of 2.01 available soon.... read more

Our first fully S/F-ed release of HOL is now
available. See the home-page at
http://hol.sf.net