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; Mon, 13 Jun 1994 12:49:46 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA20948;
          Mon, 13 Jun 1994 05:37:15 -0600
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 AA20944;
          Mon, 13 Jun 1994 05:35:48 -0600
X400-Received: by mta relay1.pipex.net in /PRMD=pipex/ADMD=pipex/C=gb/; Relayed;
               Mon, 13 Jun 1994 12:33:51 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Mon, 13 Jun 1994 12:27:47 +0100
Date: Mon, 13 Jun 1994 12:27:47 +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 0000012000000614]
X400-Content-Type: P2-1984 (2)
Content-Identifier: 614
From: K.Blackburn@win0109.wins.icl.co.uk
Message-Id: <"614*/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

Konrad is right to say that SILENT proving of alpha-convertable
subgoals is not a virtue. ProofPower tells you when it does this
step, and maintains an automatically derived label for each
subgoal, so it can usefully tell you what it has done with which
goals. This labelling helps documentation and allows one to jump
to new subgoals for exploratory purposes. Kevin Blackburn, ICL.