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 13:41:37 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23748; Thu, 22 Apr 93 05:28:34 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by ted.cs.uidaho.edu (16.6/1.34) id AA23743; Thu, 22 Apr 93 05:28:24 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57716>; Thu, 22 Apr 1993 14:28:05 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8079>; Thu, 22 Apr 1993 14:27:57 +0200 From: Konrad Slind To: info-hol@ted.cs.uidaho.edu In-Reply-To: Richard Boulton's message of Thu, 22 Apr 1993 13:36:15 +0200 <"swan.cl.cam.:284860:930422113633"@cl.cam.ac.uk> Subject: Powerful Rewriting Message-Id: <93Apr22.142757met_dst.8079@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 22 Apr 1993 14:27:56 +0200 Richard's message reminds me that there is code for some limited form of higher-order matching in the implementation of the prog_logic library (in both hol88 and hol90). Plus, if you are interested in the "Miller" subcase of higher-order unification, Tobias Nipkow has a nice paper on this, with SML source code that should be easily adaptable to HOL terms (and to matching). (Available by ftp from ftp.informatik.tu-muenchen.de, file lehrstuhl/nipkow/lics93.dvi.Z) Konrad.