Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05782-0@swan.cl.cam.ac.uk>; Tue, 7 Jul 1992 23:26:52 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04594; Tue, 7 Jul 92 15:06:18 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA04589; Tue, 7 Jul 92 15:06:12 -0700 Received: by grolsch.cs.ubc.ca id AA25784 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Tue, 7 Jul 1992 15:07:12 -0700 Date: 7 Jul 92 15:07 -0700 From: Sreeranga Rajan To: info-hol@edu.uidaho.cs.ted Message-Id: <475*sree@cs.ubc.ca> Subject: constant name reuse The problem came up when trying to use two libraries at the same time: "auxiliary" and "group" - there is a constant "INV" defined in both of them, and so loading fails complaining of constant redefinition. I was wondering if there is a solution (other than the obvious) for this: In HOL-88, for security, a constant defined in a theory may not be (re)defined in another theory, when both theories are loaded into the same HOL environment irrespective of them being ancestors of each other. This forces a book-keeping on constant definitions in various theories, and becomes even more so inconvenient in the case of libraries (created by different people). One solution to this, is probably to decorate the constants with the theory name (or perhaps use the type system to make them unique). I was wondering if this problem was being considered in future versions. Sorry, if this has come up before. Thanks for any pointers, -Sree (sree@cs.ubc.ca)