Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 29 Sep 1992 16:02:40 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07184; Tue, 29 Sep 92 06:43:01 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA07179; Tue, 29 Sep 92 06:42:50 -0700 Received: by infix.cs.ruu.nl id AA15715 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Tue, 29 Sep 1992 14:41:50 +0100 From: Wishnu Prasetya Message-Id: <199209291341.AA15715@infix.cs.ruu.nl> Subject: Inheritance of binder status To: info-hol@edu.uidaho.cs.ted (hol mailing list) Date: Tue, 29 Sep 92 14:41:49 MET X-Mailer: ELM [version 2.3 PL11] Hi, I have questions again. I have defined ?? with new_binder_definition in theory, say, X. Then I made theory Y, and declaring that X is a parent of Y. While the definition of ?? is clearly now visible in Y, it seems that the binder status is not inherited to Y. The question is, is this to be expected? Is there any special reason for this, because it seems more natural to me that such status be inherited to decendant theories, otherwise one will be obliged to always insert new_binder `XX` for each binder XX everywhere. Is there any special flag you can turn to do the trick? Thank you kindly and have a nice day. -Wishnu Prasetya- --