Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK
          with SMTP/TCP/IP over Ethernet id a007886; 27 May 89 10:04 BST
Via:  uk.ac.nsf; 27 May 89 10:03 BST  (UK.AC.Cam.Cl.scaup)
Received: from clover.ucdavis.edu by NSFnet-Relay.AC.UK   via NSFnet with SMTP
           id aa21241; 26 May 89 23:14 BST
Received: from AIR12.LARC.NASA.GOV by clover.ucdavis.edu (5.59/UCD.EECS.1.9)
        id AA13873; Fri, 26 May 89 13:03:37 PDT
Received: from localhost.ARPA by air12.larc.nasa.gov (1.2/Ultrix2.0-B)
        id AA05581; Fri, 26 May 89 16:02:03 edt
Message-Id: <8905262002.AA05581@air12.larc.nasa.gov>
To: info-hol@edu.ucdavis.clover
Subject: HOL software available on clover
Date: Fri, 26 May 89 16:01:58 EDT
From: Phil Windley <pjw@gov.nasa.larc.air12>
Sender: pjw <pjw%gov.nasa.larc.air12@edu.ucdavis.clover>
Status: R


I've recently made a few new things available on clover.  This message is
to update everyone on the software available via anonymous ftp from
clover.ucdavis.edu (128.120.57.1).

HOL-EMACS.tar.Z         Phil WIndley's HOL-GNU Emacs interface. Contains
                        a user's manual in postscript format.
HOL88.doc.Z             The document distributed with HOL.
decimal.tar.Z           Phil Windley's library for doing decimal
                        arithmetic in HOL.
franz.for.SUNOS         Information about compiling franz on SUN OS 4.
franz.tar.Z             PD Franz that is distributed with HOL
hol88.1.01.manifest     List of what's in hol88.tar.Z
hol88.tar.Z             The HOL distribution.  I took franz out an bundled
                        it separately since this file is large.
math.shar               Paul Lowenstiens math theorems and conversions for
                        existential and universal quantifiers.
microconv.ml            David Sheperd's package for doing conversions on
                        subterms (open term surgery, as he put it).
sets.tar.Z              Phil Windley's theory of finite sets.
tautal.ml               Roger Jone's ml code for proving tataulogies in HOL.

Files that end in .Z are compress and should be uncompressed using
uncompress.  Files with a .tar in them are tape archive format file that
contain more than one file (use tar to unpack).  Files that end in .shar
are shar archove format files (see the instructions at the fromt of these
files for unpacking).  Make sure that you ftp files in compressed or tar
format using binary mode.

I will have the latest release of HOL (1.05) available in the next several
weeks.  When it is, I'll send out a message to that effect.

--phil--

Phil Windley                          |  windley@clover.ucdavis.edu
Division of Computer Science          |  ucbvax!ucdavis!clover!windley
College of Engineering                |  (916) 752-7324 (or 3168)
University of California, Davis       |  Davis, CA 95616