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, 6 Jun 1994 12:48:24 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26895;
          Mon, 6 Jun 1994 05:45:24 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA26891;
          Mon, 6 Jun 1994 05:45:19 -0600
Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <00583-0@goggins.dcs.gla.ac.uk>;
          Mon, 6 Jun 1994 12:34:12 +0100
Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA07213;
          Mon, 6 Jun 94 12:34:09 BST
From: tfm@dcs.gla.ac.uk
Message-Id: <9406061134.AA07213@switha.dcs.gla.ac.uk>
To: Tobias.Nipkow@informatik.tu-muenchen.de
Cc: jug@itd.dsto.gov.au, hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: An Alternate Subgoal Package
In-Reply-To: Your message of "Mon, 06 Jun 94 08:38:25 +0100." <94Jun6.083830met_dst.8111@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 06 Jun 94 12:34:09 +0100


>> I should point out that this is not my idea, I don't know whoes it is,
>>perhaps its a well known concept.  However, as I recall it, it was related to
>> me a couple of years ago by Kevin Blackburn of ICL.
>
> The first time I came across this idea was in Isabelle, because that's
> exactly how Isabelle's subgoal package works. So I assume it is due to Larry
> Paulson.

... and is the alternative method actually better?

Tom