Taupo-4 documentation
Apart from the online documentation, the tar file for Taupo-4 does not
include any further documentation. This makes the tar file smaller.
We felt this was particularly wise as different users are unable to
read different formats and distributing all possible formats would
have been particularly wasteful.
There are three components to the official documentation:
If you use the hol98 Emacs mode, you might be interested in the one-page reference for the keybindings
it uses.
Note
Of the three official documents above, only the
Tutorial is in finished condition. The other two
still have many vestiges of HOL88 in them. We have tried to document
recent changes to the system fairly thoroughly, but documentation for
old parts of the system in these two volumes is mainly untouched.
This is not to say that it's wrong; in fact, in many cases it is still
very useful because very few functions have changed their semantics.
However, the examples for most of the old entries in the
Reference use HOL88 Classic ML syntax, which might be
rather confusing.
Please also see the release notes.
Incompatibilities with previous versions
Below is a list of some of the changes from the Taupo-3 release that
may cause users problems. The Taupo-3 release itself had a number of
incompatibilities with the
previous releases.
- The function
allow_for_overloading_on
has been
removed. All overloading functionality is done through the one
overload_on
function. Scripts should be updated by
simply removing all calls to
allow_for_overloading_on
. The resulting behaviour
should be just the same as before.
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Mon Jul 31 12:47:05 BST 2000