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:23:47 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04902;
          Fri, 4 Feb 1994 02:04:37 -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 AA04761;
          Fri, 4 Feb 1994 02:04:28 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA27362;
          Fri, 4 Feb 1994 00:58:12 -0800
Received: from skua.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 4 Feb 1994 08:57:56 +0000
To: chou@cs.ucla.edu
Cc: info-hol@cs.uidaho.edu (info-hol mailing list), Wai.Wong@cl.cam.ac.uk
Subject: Re: Finding a theorem whose name I know
In-Reply-To: Your message of "Fri, 04 Feb 94 00:10:07 PST." <9402040810.AA19254@maui.cs.ucla.edu>
Date: Fri, 04 Feb 94 08:57:50 +0000
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:270340:940204085801"@cl.cam.ac.uk>

If you know the name of the theorem, you can use either xholhelp or
the hypertext on-line reference via Mosaic. Both of them are very
very convenient.


The hard thing is when you do not know the name of a theorem. There
is a library `trs` (stand for Theorem Retrieval System). It is not
as easy to use as the utilities mentioned above, but it can search a
theorem giving it is form, e.g., if you  want the conclusion to be
in the form "x + y = y + x".

Concerning efficiency, after you accessing a theory, you can always
delete the theory cache by calling delete_cache. 

Wai