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; Tue, 24 May 1994 00:58:23 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27684;
          Mon, 23 May 1994 17:35:47 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA27680;
          Mon, 23 May 1994 17:35:46 -0600
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA29167;
          Mon, 23 May 1994 17:37:11 -0600
Message-Id: <9405232337.AA29167@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: A few new services on the HOL Information server
Date: Mon, 23 May 1994 17:37:11 -0600
From: Phil Windley <windley@lal.cs.byu.edu>


There are a few new things on the <A
HREF="http://lal.cs.byu.edu/lal/hol-documentaiton.html>HOL information
server</A>: 

1.) We have added a link that lets you finger members of the info-hol
mailing list.  The entry is next to the info-hol mailing list search link.
If you don't like how your address looks in the list, let me know and we'll
change it.

2.) The info-hol mailing list is using a new search engine that should
result in better matches.  If you tested it before, we've gotten rid of the
multiple entires problem.

3.) There are new ways of searching the HOL reference manual and the HOl
theorems.  The old ones are still the main link, the news ones are just
underneath the normal search links.  For references, the new searching is
done by keyword and description, not just the reference name.  FOr theorem,
the search is done by name *and* the theorem itself.  

Keys are given as PERL regular expressions.  This means that you can find
all theorems with LESS and ADD anywhere in their names using a REGEXP like
"LESS.*ADD|ADD.*LESS" If you're *really* brave, you can use regexps to
match patterns on the theorems themselves.  THis is actually too hard to do
by hand, but one could concieve of a front end that created the search
expression based on some simpler pattern.

Feedback, as always, is welcome.

--phil--

Phillip J. Windley, Asst. Professor              |  windley@cs.byu.edu
Laboratory for Applied Logic	                 |  
Dept. of Computer Science, TMCB 3370             |
Brigham Young University                         |  Phone: 801.378.3722
Provo UT                  84602-6576             |  Fax:   801.378.7775
------------------------------------------------------------------------
If you use WWW, I'm <A HREF="http://lal.cs.byu.edu/people/windley/windley.html">here</A>.