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 sites:

ftp.cl.cam.ac.uk, directory hvg/hol
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