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; Wed, 23 Jun 1993 16:19:31 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06349;
          Wed, 23 Jun 93 08:05:28 -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 AA06344;
          Wed, 23 Jun 93 08:05:22 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 23 Jun 1993 16:05:18 +0100
To: Victor "A." Carreno <vac@air16.larc.nasa.gov>
Cc: slind@informatik.tu-muenchen.de, info-hol@ted.cs.uidaho.edu, 
    Tom.Melham@cl.cam.ac.uk
Subject: Re: HOL portability
In-Reply-To: Your message of "Wed, 23 Jun 93 10:34:46 EDT." <9306231434.AA06115@air52.larc.nasa.gov>
Date: Wed, 23 Jun 93 16:05:13 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:080750:930623150526"@cl.cam.ac.uk>


Well, I was rather hoping more_lists would *not* just get
translated into hol90!  As a library, it's frankly a bit
of a mess (no disparagement of the author intended) and 
I was thinking we could tidy it up in the transition.

More generally, HOL90 seems to present the opportunity to
fix up various anomalies in the system.  Shouldn't we
take it?

Tom