Taupo-2 documentation
Apart from the online documentation, the tar file for Taupo-2 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-1 release that
may cause users problems. The Taupo-1 release itself had a number of
incompatibilities with the
previous Athabasca releases.
- The
Ho_theorems structure has been removed. Many
of the theorems in this structure can now be accessed in
Ho_boolTheory or boolTheory. Those
that have disappeared (e.g., RIGHT_IMP_FORALL_THM)
are typically symmetric versions of theorems in either of
Ho_boolTheory or boolTheory.
Unfortunately, there is no real rhyme or reason to the location
of these theorems. Remember to use DB.match!
- The conversion
SUC_ELIM_CONV has moved from
arithmeticTheory to numLib.
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Tue Feb 22 15:30:58 GMT 2000