Taupo-3 documentation
Apart from the online documentation, the tar file for Taupo-3 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.
Incompatibilities with previous versions
Below is a list of some of the changes from the Taupo-2 release that
may cause users problems. The Taupo-2 release itself had a number of
incompatibilities with the
previous releases.
- A number of functions in the TFL package for defining functions
(such as
WF_REL_TAC
) have changed their types since
Taupo-2. You will need to check the online documentation using
help
to bring up the signatures for the functions
that are giving you type errors.
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Tue Jun 6 12:40:12 BST 2000