Return-Path: 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 Jul 1993 22:08:15 +0100 Received: by ted.cs.uidaho.edu (16.6/2.0) id AA27136; Thu, 22 Jul 93 13:58:44 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from mahogany.cs.ucdavis.edu by cs.uidaho.edu (16.6/2.0) id AA27131; Thu, 22 Jul 93 13:58:34 -0700 Received: by mahogany.cs.ucdavis.edu (5.57/UCD.CS.2.2) id AA03309; Thu, 22 Jul 93 13:58:49 -0700 Message-Id: <9307222058.AA03309@mahogany.cs.ucdavis.edu> To: info-hol@ted.cs.uidaho.edu Subject: Re: REWRITE_TAC In-Reply-To: Your message of "Thu, 22 Jul 93 18:56:47 +0700." <9307221714.AA26293@cs.uidaho.edu> Date: Thu, 22 Jul 93 13:58:48 -0400 From: shaw@cs.ucdavis.edu X-Mts: smtp Regarding the question about REWRITE_TAC. I ran into a related situation a while back, but didn't ask about it at the time. It was a strange in case in which ASM_REWRITE_TAC[] returned a goal to which ASM_REWRITE_TAC[] still applied. That is, a second ASM_REWRITE_TAC[] further modified the goal. Perhaps someone could summarize the rewriting heuristics in a sentence or two, explaining how this comes about? Thanx Rob (Note: it may have been just plain REWRITE_TAC, I can't say for sure...)