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 05:48:08 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06052;
          Tue, 22 Jun 93 21:34:31 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06047;
          Tue, 22 Jun 93 21:34:26 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA17035;
          Tue, 22 Jun 93 21:34:49 -0700
Message-Id: <9306230434.AA17035@maui.cs.ucla.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: HOL90 is faster, for me
Date: Tue, 22 Jun 93 21:34:45 PDT
From: chou@cs.ucla.edu

Now that we are on the subject of HOL90, has anyone translated `res_quan`
and `more_lists` to HOL90?  And in general, how hard is it to translate
HOL88 libraries to HOL90?  Note that `res_quan` consists predominantly
of ML procedures, while `more_lists` is mostly theorems and proofs.
How hard would the translation be in each case?  Is there an automatic
procedure for doing the translation?  It seems plausible to me that we
can have a program that can automatically translate "Classic ML" into
Standard ML.  Or perhaps I'm just dreaming?

- Ching Tsun