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; Mon, 22 Nov 1993 17:51:55 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA21532; Mon, 22 Nov 93 10:24:53 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from panther.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA21528; Mon, 22 Nov 93 10:24:52 -0700 Received: from localhost by panther.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA19110; Mon, 22 Nov 93 10:24:52 -0700 To: info-hol@leopard.cs.byu.edu Subject: More on-line HOL services Date: Mon, 22 Nov 1993 10:24:51 -0700 From: Phil Windley Message-ID: <"swan.cl.cam.:081250:931122175259"@cl.cam.ac.uk> In an on-going effort to provide one-stop shopping for HOL information, we have added two services to the HOL WWW server on lal.cs.byu.edu: 1.) A mosaic of tech report respositories related to the HOL theorem prover and formal methods in computer system design. 2.) A list of common HOL error messages and how to resolve them If you have a tech report repository that is available via FTP or HTTP, please send me mail and I will add you to the list. Note that we don't want your technical reports, just an FTP or HTTP pointer and we'll point people at it. That way, as you update the repository and add new reports, the information service will be up to date. If you have a HOL error that is not in the list, please send me the necessary information (similar to the format shown). I *do* want the error information and I will collect it. If you haven't used WWW to look at the HOL information server, please do so. Its at http://lal.cs.byu.edu/lla/hol-documentation.html. If you need help using WWW, send us mail and we'll point you in the right direction. If you're writing a HOL library and would like to create hypertext documentation for it, we'd love to help you get started. There is an example of a hypertext documented HOL library (records) on the HOL information server and we can point you at other references that will help. HOL information services available include: o Hypertext linked, searchable HOL reference manual o Hypertext linked, searchable HOL theorems o Hypertext linked, searchable info-hol mail o On-line HOL Description Manual o On-line HOL Tutorial o On-line HOL Case Studies o Technical report repository o Error message help. o HTML HOL Document example o Information on getting HOL o FAQ list Let us know what else we can do. Cheers, --phil--