Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 26 Apr 1993 13:51:30 +0100
Received: by antares.mcs.anl.gov id AA16022 (5.65c/IDA-1.4.4 for qed-outgoing);
          Mon, 26 Apr 1993 07:40:21 -0500
Received: from sun2.nsfnet-relay.ac.uk by antares.mcs.anl.gov with SMTP 
          id AA16014 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Mon, 26 Apr 1993 07:40:10 -0500
Via: uk.ac.edinburgh.aifh; Mon, 26 Apr 1993 13:28:32 +0100
Received: from etive.aisb.ed.ac.uk by aisb.ed.ac.uk; Mon, 26 Apr 93 13:28:24 BST
Date: Mon, 26 Apr 93 13:28:23 BST
Message-Id: <28642.9304261228@etive.aisb.ed.ac.uk>
From: Alan Bundy <bundy@aisb.ed.ac.uk>
Subject: Re: Document -- What's Done and What's to be Done
To: Dewey Val Schorre <val@netcom.com>
In-Reply-To: Dewey Val Schorre's message of Sun, 25 Apr 93 15:16:35 -0700
Phone: 44-31-650-2716
Fax: 44-31-650-6516
Fcc: +qed.mai
Cc: qed@aisb.ed.ac.uk
Sender: qed-owner@mcs.anl.gov
Precedence: bulk

Val

> Someone could write nqthm as a tactic in HOL. 

	That is essentially what we have been trying to do in the
Clam/Oyster system (see Carolyn Talcott's list).  Clam contains
tactics based on Nqthm. These drive Oyster.  Oyster is a copy of
Nuprl, but it could have been HOL, and at one time we had a
project with a student of Mike Gordon's to have Clam drive HOL.
Adaption to other tactic based provers would not be too
difficult.


			Alan