Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl id <13391-0@swan.cl.cam.ac.uk>; Mon, 7 Oct 1991 16:25:13 +0100 Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (15.11/1.34) id AA19734; Mon, 7 Oct 91 08:13:00 pdt Received: by panther.cs.uidaho.edu (5.57/Ultrix3.0-C) id AA05249; Mon, 7 Oct 91 08:15:13 -0700 Message-Id: <9110071515.AA05249@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: HOL 2.0 available now Date: Mon, 07 Oct 91 08:15:11 -0700 From: Phil Windley X-Mts: smtp As the note from John mentioned, HOL 2.0 is now available from TED.CS.UIDAHO.EDU. The following gives information on obtaining the sources from TED. The /pub/hol directory contains the code for the Cambridge HOL theorem along with other auxilliary files: holdoc.tar.Z -- Documentation for HOL 2.0 holdoc.tar.Za? -- Split files for documentation for HOL 2.0 holsys.tar.Z -- HOL 2.0 System holsys.tar.Za? -- Split files for HOL 2.0 system Files with the Z extension are compressed (16-bit). Files with a tar extension are archived using tar(1). Files with a shar extension are in shar format. Please ensure that you use the binary FTP mode for transfer of compressed files. The hol{doc,sys}.tar.Z files are available in two formats. The file hol{doc,sys}.tar.Z is the complete compressed tar file. The files that match the regular expression hol{doc,sys}.tar.Za? are the compressed tar file split into 6 pieces. Unreliable FTP links sometimes make retrieving a large file tenuous. To untar the split files use the following command: cat hol{doc,sys}.tar.Za? |uncompress |tar -xvf - Note that zcat cannot be used (try it to find out why; you won't break anything). If you need additional help getting the HOL system or desire to recieve the system by tape rather than FTP, send mail to windley@panther.cs.uidaho.edu. --phil--