Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Message-Id: <9310012142.AA21595@laforge>
To: info-hol@cs.uidaho.edu
Cc: mbarnett@cs.uidaho.edu, foster@cs.uidaho.edu
Subject: A New on-line HOL Documentation Service!!!!
Date: Fri, 01 Oct 93 15:42:37 -0600
From: Phil Windley <windley@laforge.cs.byu.edu>


The Laboratory for Applied Logic at Brigham Young University is pleased to
announce the opening of an on-line network hypertexted based documentation
service for the HOL theorem proving system.  Using this service, you will
be able to access HOL documentation in hypertext format.

To browse this documentation, you will first need to obtain the XMosaic
tool.  This tool is freely distributed by NCSA.  To get the tool, use
anonymous FTP to connect to ftp.ncsa.uiuc.edu.  In the directory
/Mosaic/xmosaic-binaries you will find already compiled copies of the
latest version of XMosaic for a variety of architectures.  The source code
is available in /Mosaic/xmosaic-source.

While, you're there, download the papers in /Mosaic/mosaic-papers and read
them.  They will provide you with additional information about XMosaic.

The on-line documentation service is available at URL

    http://lal.cs.byu.edu/lal/hol-documentation.html.

Select OPEN from the XMosaic menu and enter this line.  You will then be
connected to the HOL documentation server.

In the near future we will be distributing the code necessary for you to
run this server locally if the network access is too slow.  Please stay
tuned for further details.

Please direct any comments to:

Phillip J. Windley, Asst. Professor   |  windley@cs.byu.edu
Laboratory for Applied Logic	      |  
Dept. of Computer Science, TMCB 3370  |
Brigham Young University              |  Phone: 801.378.3722
Provo UT       84602-6576             |  Fax:   801.378.7775