Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP (PP-6.5) 
          id <29731-0@swan.cl.cam.ac.uk>; Thu, 9 Jun 1994 09:37:13 +0100
Received: from leopard.cs.byu.edu by sun3.nsfnet-relay.ac.uk with Internet SMTP 
          id <sg.29880-0@sun3.nsfnet-relay.ac.uk>;
          Thu, 9 Jun 1994 09:36:56 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA18948;
          Thu, 9 Jun 1994 02:26:03 -0600
Original-Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from relay1.pipex.net by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA18944;
          Thu, 9 Jun 1994 02:25:51 -0600
X400-Received: by mta relay1.pipex.net in /PRMD=pipex/ADMD=pipex/C=gb/; Relayed;
               Thu, 9 Jun 1994 09:23:22 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Thu, 9 Jun 1994 09:17:18 +0100
Date: Thu, 9 Jun 1994 09:17:18 +0100
X400-Originator: K.Blackburn@win0109.wins.icl.co.uk
X400-Recipients: hol2000@lal.cs.byu.edu
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012000000607]
X400-Content-Type: P2-1984 (2)
Content-Identifier: 607
From: K.Blackburn@win0109.wins.icl.co.uk
Message-Id: <"607*/I=K/S=Blackburn/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: hol2000@leopard.cs.byu.edu
Subject: Re: Alternate Subgoal Packages
Sender: hol2000-request@lal.cs.byu.edu

A minor advantage to holding the subgoal package state as a
theorem is that certain manipulations become possible. Easily
the most useful is that you can eliminate duplicated subgoals in
a sound manner because they are represented as alpha-equivalent
assumptions.
Kevin Blackburn, ICL