Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Sun, 22 Nov 1992 09:44:49 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06035; Sun, 22 Nov 92 01:28:46 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA06030; Sun, 22 Nov 92 01:28:40 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA06584; Sun, 22 Nov 92 01:28:01 -0800 Message-Id: <9211220928.AA06584@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: Fast retrieval of NAMES of definitions and theorems? Date: Sun, 22 Nov 92 01:28:00 PST From: chou@edu.ucla.cs Is there any way of retrieving the names of definitions and theorems of an ancestor theory without retrieving at the same time the corresponding thm's? The only way of retrieving names that I know of is to use the ML functions `definitions` amd `theorems`, which get not only the names but also the thm's and are terribly slow when the thm's contain large terms. - Ching Tsun