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; Fri, 10 Feb 1995 15:52:14 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA18053;
          Fri, 10 Feb 1995 08:24:44 -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 AA18040;
          Fri, 10 Feb 1995 08:24:22 -0700
Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl;
          Fri, 10 Feb 1995 15:22:08 +0000
X-Mailer: exmh version 1.5.2 12/21/94
To: info-hol@leopard.cs.byu.edu
Subject: new_parent bugs in hol90.7 and hol88 2.02
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Fri, 10 Feb 1995 15:22:03 +0000
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:122640:950210152212"@cl.cam.ac.uk>


Dear fellow HOL hackers,

Two things relating to new_parent:

1. In hol88, the parent list can be made to contain duplicates by
using new_parent twice with the same name.  Should this be fixed?

e.g.

albatross.cl.cam.ac.uk:Fri Feb 10 > hol88

#new_theory `test`;;
new_parent () : void

#`HOL`;;
Theory HOL loaded
() : void

#parents `-`;;
[`HOL`; `HOL`] : string list


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

e.g.

> hol90
...
The library "HOL" is loaded.
- new_theory "test1";

Declaring theory "test1".

Theory "HOL" already consistent with disk, hence not exported.
val it = () : unit
- new_theory "test2";

Declaring theory "test2".

Theory "test1" exported.
val it = () : unit
- new_parent "HOL";
val it = () : unit
- parents "-";
val it = ["test1"] : string list
- 


In hol88 the parents whould contain test1 and HOL.

Thanks,
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
-----------------------------------------------------------------------------