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, 3 Nov 1994 16:47:16 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA16895;
          Thu, 3 Nov 1994 09:39:03 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from catseye.idbsu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA16891;
          Thu, 3 Nov 1994 09:39:02 -0700
Received: by catseye.idbsu.edu (1.38.193.4/16.2) id AA12049;
          Thu, 3 Nov 1994 09:31:53 -0700
Date: Thu, 3 Nov 1994 09:31:53 -0700
From: Randall Holmes <holmes@catseye.idbsu.edu>
To: info-hol@leopard.cs.byu.edu, murthy@cs.cornell.edu
Subject: Translation
Message-ID: <"swan.cl.cam.:030760:941103164919"@cl.cam.ac.uk>


I _did_ translate my prover into Caml Light; it was essentially a
mechanical task, but I wouldn't want to have to do it again.  Could
a computer program be written which would give at least a first
approximation to this translation?

					--Randall Holmes

(it was originally in sml)