Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 9 Dec 1992 10:49:51 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13894; Wed, 9 Dec 92 01:12:19 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13889; Wed, 9 Dec 92 01:12:10 -0800 Received: from razorbill.cl.cam.ac.uk (user jg (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Wed, 9 Dec 1992 09:11:27 +0000 To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs (Ching-Tsun Chou) Subject: Re: **** RELEASE OF HOL 2.01 **** In-Reply-To: Your message of Tue, 08 Dec 92 16:35:39 -0800. <9212090035.AA12293@maui.cs.ucla.edu> Date: Wed, 09 Dec 92 09:11:21 +0000 From: Jim Grundy Message-Id: <"nene.cl.ca.528:09.12.92.09.11.28"@cl.cam.ac.uk> >> o Renaming of REWRITE_CONV to REWR_CONV (see below); >> there is an entry "newrw" in "contrib" to update code with respect >> to this change. > > What is the rationale behind this change? > > - Ching Tsun I think I best answer this since I am the one responsible. HOL2.0 contained lots of rewriting rules and tactics: GEN_REWRITE_RULE, GEN_REWRITE_TAC, REWRITE_RULE, REWRITE_TAC, ..., but no analagous conversions. In my own work (and I know in the work of others since I ripped off their code) I found it was useful to have these conversions - but what to call them? In the end it was felt better to call them GEN_REWRITE_CONV, REWRITE_CONV,... to preserve the intuition that these conversions are analogous to the rewriting rules and tactics. It was then necessary to find a new name for the old REWRITE_CONV. I think this was a good move anyway since the old name erroneously suggested that it was analogous to REWRITE_RULE and REWRITE_TAC, which it wasn't. Hence it is now called REWR_CONV - shorter, more primitive. As it happens adding these functions has allowed a nicer implementation of the rewriting rules and tactics in terms of the rewriting conversions. I think this is the way it should have been done in the beginning. I do apologise to those of you who are going to be inconvenienced by having to go though your code and change instances of REWRITE_CONV to REWR_CONV. I hope, however, that the script "newrw" in contrib will make this task a lot less tiresome. Jim =============================================================================== Jim Grundy University of Cambridge | Phone: +44 223 334760 | This space has Computer Laboratory | Fax: +44 223 334678 | been intentionally New Museums Site | Telex: CAMSPLG 81240 | left blank for Pembroke Street | email: jg@cl.cam.ac.uk | formatting Cambridge CB2 3QG | | purposes. UNITED KINGDOM | | ===============================================================================