Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <17673-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 16:06:03 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15659;
          Mon, 9 Mar 92 07:39:44 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA15555;
          Mon, 9 Mar 92 07:39:33 -0800
Received: from antiphos.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation)
          id AA01356; Mon, 9 Mar 92 10:40:43 EST
Date: Mon, 9 Mar 92 10:40:40 EST
From: hoove@com.oracorp
Received: by antiphos.oracorp.com (4.1/1.3-ORA Corporation) id AA02252;
          Mon, 9 Mar 92 10:40:40 EST
Message-Id: <9203091540.AA02252@antiphos.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: rewriting in HOL

A couple of questions relating to rewriting.

1. Does anyone have tactics for conditional rewriting?

2. Has anyone collected reasonably general, but terminating collections
   of rewrite rules for natural numbers, integers, other algebraic
   structures.

thanks and regards,

Doug Hoover
hoove@oracorp.com