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 23:20:34 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07857; Fri, 16 Apr 93 15:09:10 -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 AA07852; Fri, 16 Apr 93 15:09:05 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 16 Apr 1993 23:08:45 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Forcing precedence in rewrites Date: Fri, 16 Apr 93 23:08:34 +0100 From: John Harrison Message-Id: <"swan.cl.ca.879:16.04.93.22.09.00"@cl.cam.ac.uk> I have a related question to Steve's: suppose you have a list of theorems [th1; ...; thn] and you want to apply them as rewrite rules with some search strategy or other. You can do something like: REWRITE_RULE [th1; ...; thn] or GEN_REWRITE_RULE DEPTH_CONV [] [th1; ...; thn] However none of the inbuilt rewriting tools seem to guarantee that at any subterm, the *first* applicable equation in the list will be applied preferentially. Of course you could do something like: CONV_RULE (DEPTH_CONV (FIRST_CONV (map REWR_CONV [th1; ...; thn]))) but I suspect it would be much less efficient than the optimized general functions. Is there a convenient way of doing this? John.