Path: neptune!arp.anu.edu.au!reasoning-owner@arp.anu.edu.au
Posted-Date: Mon, 04 Mar 91 10:15:02 +0000
Original-To: info-hol@clover.ucdavis.edu
Subject: HOL 1.12 release
Date: Mon, 04 Mar 91 10:15:02 +0000
From: Sara.Kalvala@computer-lab.cambridge.ac.uk
Message-ID: <"swan.cl.ca.797:04.02.91.10.15.07"@cl.cam.ac.uk>
Original-Resent-To: reasoning-people
Original-Resent-Reply-To: Sara.Kalvala@computer-lab.cambridge.ac.uk
Newsgroups: anu.reasoning
Distribution: anu
Sender: postmaster@arp.anu.edu.au
Approved: anu.reasoning@arp.anu.edu.au



[ My last message seems to have bounced at a few sites, so here it
  goes again. Apologies to those who already got it.        - Sara ]

----



A new version of HOL has been released this week. HOL1.12 has
substantial improvements over version 1.11 - the code has been cleaned
up significantly, and resolution-based tactics have been rationalized,
among other things.

The documentation is still from 1.11. New documentation is almost
ready, and we will put out a new release of the system when it
is.  The code for HOL should not change (except for bugfixes) in a
significant manner between the two releases.

There are two ways you can obtain HOL1.12:

- tape: I can put the sources (tar format) on tape if you send me a
   blank at the address below;

- ftp: anonymous ftp from the pub directory at cs.uidaho.edu
   (129.101.100.20) which contains the file HOL12.tar.Z (4Mb).

The current ftp site (clover.ucdavis.edu) is about to be retired, so
until a new machine at UCDavis is allocated for anonymous ftp Phil has
made the sources available at cs.uidaho.edu.

Please let me know if there are any problems with obtaining or
building the sources. And happy theorem proving!


					- Sara Kalvala
					sk@cl.cam.ac.uk

					University of Cambridge
					Computer Laboratory
					New Museums Site, Pembroke St.
					Cambridge CB2 3QG
					ENGLAND