Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <18769-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 16:50:57 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23545; Mon, 9 Mar 92 08:36:45 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA23469; Mon, 9 Mar 92 08:36:34 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <18502-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 16:38:32 +0000 To: hoove@com.oracorp Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: rewriting in HOL In-Reply-To: Your message of Mon, 09 Mar 92 10:40:40 -0500. <9203091540.AA02252@antiphos.oracorp.com> Date: Mon, 09 Mar 92 16:38:28 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.506:09.02.92.16.38.35"@cl.cam.ac.uk> > 1. Does anyone have tactics for conditional rewriting? See the contrib directory called "rewriting". Tom