Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sun, 30 May 1993 15:04:15 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04391;
          Sun, 30 May 93 06:50:48 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA04386;
          Sun, 30 May 93 06:50:34 -0700
Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Sun, 30 May 1993 14:50:42 +0100
To: info-hol@ted.cs.uidaho.edu
Subject: Announcing a new HOL library --- word
Date: Sun, 30 May 93 14:50:33 +0100
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:016270:930530135045"@cl.cam.ac.uk>


	A new HOL library `word` for modelling bit vectors has been
added to the next version (2.02) of HOL88. A complete manual is
included. It is also available for HOL88 version 2.01 via anonymous
ftp from Cambridge in the contrib directory. This library requires
the res_quan library to work. So remember to fetch that as well.

	The porting of these libraries, word and res_quan, to HOL90
are in progress. Further information will be announced in due course.

Wai