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, 26 May 1994 14:32:13 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA24357;
          Thu, 26 May 1994 07:25:54 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from cornell.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA24353; Thu, 26 May 1994 07:25:53 -0600
Received: from msiadmin.cit.cornell.edu ([128.253.216.2]) by cornell.edu 
          with SMTP id <577593-7>; Thu, 26 May 1994 09:25:51 -0400
Date: Thu, 26 May 1994 09:25:27 -0400
From: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Received: from msipawn.409col_ave by msiadmin.cit.cornell.edu (4.1/1.5) 
          id AA13296; Thu, 26 May 94 09:25:27 EDT
Message-Id: <9405261325.AA13296@msiadmin.cit.cornell.edu>
To: hol2000@leopard.cs.byu.edu
Subject: What's up for grabs?
Cc: garrel@msiadmin.cit.cornell.edu

I have a bunch of ideas that might be relevant to putting together HOL2000.
But it's not clear to me which of my ideas really are relevant, because I'm
not sure what kinds of changes the following statement from the hol2000
announcement rules out:

  The goal would be to put together a design for the next generation of
  HOL-like theorem proving environments. This should not be a redesign
  from first principles, but an evolution from the current state done in
  a framework that preserves the existing HOL implementations as
  workhorses for the rest of the decade.

Would somebody like to take a stab at clarifying that?

Regards,

Garrel