Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Mon, 18 Jan 1993 10:06:28 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08900; Mon, 18 Jan 93 00:54:21 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08895; Mon, 18 Jan 93 00:54:15 -0800 Received: from caxton.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Mon, 18 Jan 1993 08:53:32 +0000 To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list), Tom.Melham@uk.ac.cam.cl Subject: Re: RULE_ASSUM_TAC: a suggestion In-Reply-To: Your message of Sun, 17 Jan 93 22:07:00 -0800. <9301180607.AA10190@maui.cs.ucla.edu> Date: Mon, 18 Jan 93 08:53:26 +0000 From: Tom Melham Message-Id: <"swan.cl.ca.029:18.01.93.08.53.38"@cl.cam.ac.uk> > I suggest that RULE_ASSUM_TAC use CHECK_ASSUME_TAC instead of ASSUME_TAC: That certainly looks like a sensible possibility. However, with any non-compatable change of this kind one has to consider carefully how many users will be annoyed by it. In some cases it's better just to define your own private function with the desired behaviour. Tom