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 15:10:03 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23784;
          Thu, 22 Apr 93 06:53:57 -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 AA23779;
          Thu, 22 Apr 93 06:53:28 -0700
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 22 Apr 1993 14:51:09 +0100
To: info-hol@ted.cs.uidaho.edu
Subject: Powerful Rewriting
Date: Thu, 22 Apr 93 14:51:02 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:026940:930422135121"@cl.cam.ac.uk>


Higher-order unification and matching is standard in Isabelle's implementation
of HOL.  It is efficient too.

							Larry Paulson