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 07:43:26 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA24973;
          Mon, 6 Jun 1994 00:40:57 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA24937;
          Mon, 6 Jun 1994 00:39:54 -0600
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <326456>;
          Mon, 6 Jun 1994 08:38:55 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8111>;
          Mon, 6 Jun 1994 08:38:30 +0200
From: Tobias.Nipkow@Informatik.TU-Muenchen.De
To: jug@itd.dsto.gov.au
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <9406060621.AA21012@itd0.dsto.gov.au> (message from Jim Grundy on Mon, 6 Jun 1994 08:21:42 +0200)
Subject: Re: An Alternate Subgoal Package
Message-Id: <94Jun6.083830met_dst.8111@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 6 Jun 1994 08:38:25 +0200

Jim Grundy writes:

> 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.

Tobias