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; Thu, 1 Sep 1994 13:02:45 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10636;
          Thu, 1 Sep 1994 05:44:59 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-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 AA10632;
          Thu, 1 Sep 1994 05:44:57 -0600
Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <08010-0@goggins.dcs.gla.ac.uk>;
          Thu, 1 Sep 1994 12:39:35 +0100
Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA22903;
          Thu, 1 Sep 94 12:39:33 BST
From: tfm@dcs.gla.ac.uk
Message-Id: <9409011139.AA22903@switha.dcs.gla.ac.uk>
To: info-hol@leopard.cs.byu.edu
Cc: tfm@dcs.gla.ac.uk
Subject: LaTeX-ing the HOL manual.
Date: Thu, 01 Sep 94 12:39:33 +0100

Users may have noticed that the HOL documentation does not typeset
cleanly using LaTeX2e, which is the official replacement for LaTeX2.09.
The trouble is in the following lines 

   \setlength{\mathindent}{\tabcolsep}
   \addtolength{\mathindent}{\the\fontdimen2\elvtt}
   \addtolength{\mathindent}{\the\fontdimen2\elvtt}
   \addtolength{\mathindent}{\the\fontdimen2\elvtt}

which occur in the layout file

   <hol-root-directory>/Manual/LaTeX/layout.sty
   
The fix is to change these lines to the following

   \setlength{\mathindent}{\tabcolsep}
   \newbox\temp
   \setbox\temp=\hbox{\small\verb!   !}
   \addtolength{\mathindent}{\wd\temp}

Tom