Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 22 Mar 1994 16:05:50 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27657; Tue, 22 Mar 1994 08:43:14 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA27645; Tue, 22 Mar 1994 08:42:54 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 22 Mar 1994 15:42:33 +0000 To: info-hol@leopard.cs.byu.edu Subject: **** RELEASE OF HOL88 2.02 **** Date: Tue, 22 Mar 94 15:42:28 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:286000:940322154240"@cl.cam.ac.uk> 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://lal.cs.byu.edu/pub/hol (Site "lal.cs.byu.edu", directory "pub/hol") ftp://ftp.cl.cam.ac.uk/hvg/hol (Site "ftp.cl.cam.ac.uk", directory "hvg/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