Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 8 Sep 1992 18:59:33 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15677; Tue, 8 Sep 92 10:12:17 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from utrhcs.cs.utwente.nl by ted.cs.uidaho.edu (16.6/1.34) id AA15672; Tue, 8 Sep 92 10:11:48 -0700 Received: from perseus.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.3mx) id AA06041; Tue, 8 Sep 92 19:10:26 +0200 Received: from utis143.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0) id AA06528; Tue, 8 Sep 92 19:10:24 +0200 Date: Tue, 8 Sep 92 19:10:24 +0200 From: vdvoort@nl.utwente.cs (Mark van de Voort) Message-Id: <9209081710.AA06528@perseus.cs.utwente.nl> To: info-hol@edu.uidaho.cs.ted Subject: Re: short query In-Reply-To: Mail from 'Sreeranga Rajan ' dated: 8 Sep 92 9:50 -0700 S> Thanks. But, the problem lies in identifying the theorem associated with S> define_type - which introduces the type constructors. S> So, my query was - is there a better way than a naming convention S> for this identification? As much as I dislike side-effects in an language, I'd resort to one in this case. Start your session with: # letref def_types :(thm)list = [];; #let new_define_type str1 str2 = # let tmpth = (define_type str1 str2) # in def_types := tmpth.def_types; tmpth ;; and use new_define_type instead of define_type. It should be easy to distill the constructors from the theorems held in def_types. Of course this is just a quick and dirty solution. Mark.