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; Fri, 4 Feb 1994 09:25:19 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA05289;
          Fri, 4 Feb 1994 02:08:42 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA05285;
          Fri, 4 Feb 1994 02:08:36 -0700
Received: from concorde.inria.fr by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA27374;
          Fri, 4 Feb 1994 01:04:50 -0800
Received: from pauillac.inria.fr by concorde.inria.fr;
          Fri, 4 Feb 1994 10:04:37 +0100
Received: from localhost.inria.fr by pauillac.inria.fr;
          Fri, 4 Feb 94 10:04:35 +0100
To: chou@cs.ucla.edu
Cc: info-hol@cs.uidaho.edu (info-hol mailing list), murthy@pauillac.inria.fr
Subject: Re: Finding a theorem whose name I know
In-Reply-To: Your message of Fri, 04 Feb 1994 00:10:07 -0800. <9402040810.AA19254@maui.cs.ucla.edu>
Date: Fri, 04 Feb 1994 10:04:33 +0100
Message-Id: <25990.760352673@pauillac.inria.fr>
From: Chet Murthy <Chet.Murthy@inria.fr>


Chances are, a tags-like facility is enough for now.  There was a
package once called "mkid" which was a sort of generalized tags
facility for an arbitrary language.

--chet--