Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 22 Apr 1993 12:49:48 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23730; Thu, 22 Apr 93 04:40:52 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA23725; Thu, 22 Apr 93 04:40:35 -0700 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 22 Apr 1993 12:36:25 +0100 To: schneide Cc: info-hol@ted.cs.uidaho.edu Subject: Re: Powerful Rewriting In-Reply-To: Your message of Thu, 22 Apr 93 08:22:37 +0700. <9304220621.AA23277@ted.cs.uidaho.edu> Date: Thu, 22 Apr 93 12:36:15 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:284860:930422113633"@cl.cam.ac.uk> Klaus Schneider writes: > Has anyone implemented rules, conversions or tactics for a more powerful > rewriting? For example, associative and commutative rewriting would in > some cases be helpful. Moreover, HOL's rewriting does only first-order > matching, in some cases higher-order matching would be more useful. > Last but not least I would like to know who has experience with E-unification > in HOL? I have written code to perform a restricted form of higher-order matching. Richard.