Return-Path: 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 Feb 1995 10:35:59 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA27000; Mon, 13 Feb 1995 03:20:55 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA26996; Mon, 13 Feb 1995 03:20:54 -0700 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 13 Feb 1995 10:17:30 +0000 X-Mailer: exmh version 1.5.2 12/21/94 To: info-hol@leopard.cs.byu.edu Subject: Re: new_parent bugs in hol90.7 and hol88 2.02 In-Reply-To: Your message of "Fri, 10 Feb 1995 18:24:47 +0100." <95Feb10.182454met.8081@sunbroy14.informatik.tu-muenchen.de> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Mon, 13 Feb 1995 10:17:25 +0000 From: Donald Syme Message-Id: <"swan.cl.cam.:095140:950213101737"@cl.cam.ac.uk> Konrad sent the following reply directly to me (it didn't seem to come via info-hol, so I thought I would include it here). > > > In hol90.7, new_parent doesn't seem to work if the specified parent > > is already an ancestor of the current theory. This is different to > > hol88. Is this a bug or a feature? > > I would say that it's the correct behaviour; "new_parent" ought to do > nothing if the nominated theory is already an ancestor. Maybe a wrapper > routine around "new_parent" like the following would be helpful. > ... I'm not sure about this. The best reason to directly add a parent which is already an ancestor is for clarity - i.e. to show that a theory uses another theory directly, and not merely as an artifact of it being an ancestor via a third theory. Ancestors are different from parents, right? For instance they will be shown differently in a graphical representation of the theory tree. The HOL theory tree tends to represent the implementation of the HOL logic rather than the user's preception of the logic. Adding new parents is one of the only ways of adjusting the theory tree to reflect the real logical structure. It's obviously not very important though. BTW, has the principle of attempting compatability with the hol88 documentation been dropped? Just wondering. Cheers, Donald Syme ----------------------------------------------------------------------------- At the lab: At home: The Computer Laboratory c/o Trinity Hall New Museums Site CB2 1TJ University of Cambridge Cambridge, UK CB4 3BD Cambridge, UK -----------------------------------------------------------------------------