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, 17 Jun 1994 17:49:42 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28017;
          Fri, 17 Jun 1994 08:47:49 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28013;
          Fri, 17 Jun 1994 08:47:35 -0600
Received: from annenkov.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <11638-0@goggins.dcs.gla.ac.uk>;
          Fri, 17 Jun 1994 15:44:37 +0100
Received: by annenkov.dcs.gla.ac.uk (4.1/Dumb) id AA05227;
          Fri, 17 Jun 94 15:44:30 BST
Date: Fri, 17 Jun 94 15:44:30 BST
From: konrad@dcs.gla.ac.uk
Message-Id: <9406171444.AA05227@annenkov.dcs.gla.ac.uk>
To: info-hol@leopard.cs.byu.edu, des@inmos.co.uk
Cc: reetz@ira.uka.de
In-Reply-To: David Shepherd's message of Fri, 17 Jun 1994 10:53:19 +0200 <1632.9406170853@frogland.inmos.co.uk>
Subject: how fast is hol90's function theorem?


Many of the functions that hol90 uses to find things use linear search
when hashing on strings (for instance) might be quicker for large lists.
I confess that I hadn't imagined that it would be a bottleneck!

Question: should the source code to HOL2000 be browsable with mosaic? I
imagine that putting all the links in would be a lot of work, but then
again, many users seem to end up perusing the sources (to track down
bugs, reuse code, etc.)

Konrad.