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