Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 07:32:50 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23283;
          Wed, 21 Apr 93 23:22:06 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA23277;
          Wed, 21 Apr 93 23:21:52 -0700
Message-Id: <9304220621.AA23277@ted.cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <25801-0@iraun1.ira.uka.de>; Thu, 22 Apr 1993 08:21:37 +0200
Date: Thu, 22 Apr 93 8:22:37 MET DST
From: schneide <schneide@ira.uka.de>
To: info-hol@ted.cs.uidaho.edu
Subject: Powerful Rewriting


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?

Klaus