Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 14 Jun 1994 14:12:17 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01062; Tue, 14 Jun 1994 07:09:16 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA01057; Tue, 14 Jun 1994 07:05:48 -0600 Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <13667-0@goggins.dcs.gla.ac.uk>; Tue, 14 Jun 1994 14:03:32 +0100 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA15975; Tue, 14 Jun 94 14:03:15 BST From: tfm@dcs.gla.ac.uk Message-Id: <9406141303.AA15975@switha.dcs.gla.ac.uk> To: reetz Cc: hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Re: Improved error messages In-Reply-To: Your message of "Mon, 13 Jun 94 16:51:15 EDT." <"i80fs2.ira.801:13.05.94.14.51.22"@ira.uka.de> Date: Tue, 14 Jun 94 14:03:14 +0100 > It would be helpful if HOL_ERR would output > the terms causing the failure, too. Otherwise,... What happens when you're doing, say, a Microprocessor proof and the terms you're dealing with are several pages long? Tom