Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 8 Sep 1994 07:49:48 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA26475;
          Thu, 8 Sep 1994 00:44:48 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA26471;
          Thu, 8 Sep 1994 00:44:43 -0600
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <326474>;
          Thu, 8 Sep 1994 08:40:17 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8082>;
          Thu, 8 Sep 1994 08:39:11 +0200
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, toshok@cs.uidaho.edu
In-Reply-To: <199409080059.RAA06302@wilson.cs.uidaho.edu> (message from Chris Toshok on Thu, 8 Sep 1994 02:59:12 +0200)
Subject: Re: Libraries being ported for HOL90?
Message-Id: <94Sep8.083911met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 8 Sep 1994 08:39:09 +0200


>  I was wondering if anyone was currently working on porting any of the
> libraries from HOL88 to HOL90.  I need a few for some work I'm doing,
> and if no one is currently doing the ones I need, I'll probably give
> them a shot.

Paul Curzon has ported the libraries

     cond_rewr
     res_quan
     word

to hol90 and they should be available soon. Paul has also extensively
augmented the built-in theory of lists.

Others are currently working on the records library and the finite sets
library.

Konrad.