Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Fri, 16 Apr 1993 19:37:54 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06838; Fri, 16 Apr 93 11:28:14 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06833; Fri, 16 Apr 93 11:28:08 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 16 Apr 1993 19:27:18 +0100 To: shb@com.oracorp Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: Rewriting speed In-Reply-To: Your message of Fri, 16 Apr 93 12:45:43 -0400. <9304161645.AA13795@sparta.oracorp.com> Date: Fri, 16 Apr 93 19:27:12 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.351:16.04.93.18.27.24"@cl.cam.ac.uk> There's a thing in HOL88 called "discrimination nets" which is used to speed up rewriting. They are a form of quick look-up for theorems that match the thing to be rewritten, and experiments I've done have shown that they do indeed speed things up. To get the benefit of these, without digging down into the messy details, use the recently added rewriting conversions --- REWRITE_CONV, etc. Tom