HOL 88 V 2.02
=============

The HOL system is an interactive theorem prover for higher-order logic.

Version 2.02 of HOL88 ("Classic" HOL) is now available. This version
incorporates relatively few substantial changes, but several bugs (one serious)
have been fixed and a few optimizations included. Here is a list of some of the
more significant changes.

  Extensive new facilities for proof recording (for use in conjunction with
  proofcheckers) have been installed.

  The list theory in the core has been substantially extended and regularized.

  The following new libraries have been added:

   res_quan     Wai Wong          Dealing with restricted quantifiers
   word         Wai Wong          Modelling bit vectors
   record_proof Wai Wong          Proof recording
   numeral      Tim Leonard       Dealing with large numbers in arbitrary bases

  Other libraries which did not have `standard' documentation have been moved
  to contrib. Apart from these, the following contrib entries are new:

   int            John Harrison     Integers theory

   mweb           Wishnu Prasetya   The mweb source management utilities

   Predicate      Wishnu Prasetya   Theory of lifted predicates in HOL

   rec_tys_listop Brian Graham      Extension to recursive type definition

   AKCL-profiling John Van Tassel   Rudimentary profiling utility for AKCL

   reduct         John Harrison     R/S/T closure; abstract reduction relations

   greatest       Catia Angelo      Theory about greatest of a list of numbers

   sml-mode       Wai Wong          SML mode for gnuemacs Version 19.XX

   HOLproof       Joakim von Wright Formalisation of HOL proofs in HOL

   Z              Mike Gordon       Shallow embedding of Z in HOL

   RefCalc        Joakim von Wright Program verification and refinement

   pre-v2.02-rewr Richard Boulton   Compatibility files for old rewriting

HOL can be obtained by anonymous FTP from either of the following two
addresses:

  ftp://ftp.cl.cam.ac.uk/hvg/hol (Site "ftp.cl.cam.ac.uk", directory "hvg/hol")

  ftp://lal.cs.byu.edu/pub/hol (Site "lal.cs.byu.edu", directory "pub/hol")

The two main files are "holsys.tar.gz" and "holdoc.tar.gz", which are gzipped
tarfiles of, respectively, the HOL system (i.e. code, theories) and the HOL
documentation (help files and stuff to build the manuals). There are other odds
and ends available too, mostly concerned with particular LISPs. Users who do
not have "gzip" to unpack these files may find that too at the above-mentioned
sites.

Answers to queries and requests for more information, or help with problems in
getting hold of HOL, may be received by emailing:

  hol-support@cl.cam.ac.uk

or by contacting me personally (see details below). Delivery of HOL on magnetic
tape can be arranged for users without FTP access.

Regards,

  John Harrison (jrh@cl.cam.ac.uk)

  Hardware Verification Group
  University of Cambridge Computer Laboratory
  New Museums Site
  Pembroke Street
  Cambridge CB2 3QG
  England.

  Phone: +44 223 334729
  Fax:   +44 223 334678