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; Tue, 11 Oct 1994 10:47:46 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA09498;
          Tue, 11 Oct 1994 03:52:08 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA09494;
          Tue, 11 Oct 1994 03:51:59 -0600
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Tue, 11 Oct 1994 10:45:20 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <28469-0@i80fs2.ira.uka.de>;
          Tue, 11 Oct 1994 10:48:39 +0100
Date: Tue, 11 Oct 94 10:48:39 EST
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: RE: adding definitions to closed theories
Message-Id: <"i80fs2.ira.472:11.10.94.09.48.50"@ira.uka.de>

David Shepherd writes:

>I think the problem here is that HOL maintains a global name
>space for constants. Adding definitions can cause problems
>as consider a theory TH1 which has as parents TH2 and TH3.
>If indenpendently new definitions are added to TH2 and TH3
>which each define the same name then there will be a clash
>in TH1. If constants were identified by a pair of defining theory
>and name then this might be less of a problem.

Another solution may be overloaded constants, i.e. in TH2
a constant foo:type1 and in TH1 a constant foo:type2 can
defined. Anyway, if I want to add a new constant to e.g. TH2,
I don't see a problem in looking throw the WHOLE theory tree
and not only to the parents of TH2 in searching for an
(hopefully) not already existing constant of the same name.

Ralf.

(**************************************************************)
(*                                                            *)
(*  Ralf Reetz                                                *)
(*                                                            *)
(*  University of Karlsruhe                                   *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz           *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany         *)
(*                                                            *)
(*  e-mail: reetz@ira.uka.de                                  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html  *)
(*                                                            *)
(**************************************************************)