Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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:28:50 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01148;
          Tue, 14 Jun 1994 07:25:29 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA01140;
          Tue, 14 Jun 1994 07:25:23 -0600
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Tue, 14 Jun 1994 15:18:12 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <29395-0@i80fs2.ira.uka.de>;
          Tue, 14 Jun 1994 15:24:36 +0200
Date: Tue, 14 Jun 94 15:24:35 EDT
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: long error messages
Message-Id: <"i80fs2.ira.399:14.05.94.13.24.47"@ira.uka.de>

>What happens when you're doing, say, a Microprocessor proof
>and the terms you're dealing with are several pages long?

Use a flag to control the following:

the error-message might optionally written into a text-file.

Ralf.