Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-5.6)
          id <25662-0@swan.cl.cam.ac.uk>; Fri, 29 Nov 1991 12:05:42 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA26072;
          Fri, 29 Nov 91 03:53:54 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (15.11/1.34) id AA26068;
          Fri, 29 Nov 91 03:53:45 pst
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-5.6) to cl
          id <25412-0@swan.cl.cam.ac.uk>; Fri, 29 Nov 1991 11:53:55 +0000
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: bug in version 2.0 REFERENCE manual.
Date: Fri, 29 Nov 91 11:53:52 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.414:29.10.91.11.53.57"@cl.cam.ac.uk>


Unfortunately, the LaTeX source for the REFERENCE manual sent out with version
2.0 has a bug which prevents the second chapter (built-in theorems) and the
index from printing.  The \include commands for chapter 2 and for the index
were inadvertently commented out!

To patch, change the last few commented-out lines in the LaTeX source of
hol/Manual/Reference/reference.tex to:

   \include{theorems}                    % pre-proved theorems

   {\def\#{\char'043}                    % \tt style `#' character
    \cleardoublepage
    \include{index}}

Then retypeset REFERENCE by doing "make all".  If you have already printed it,
you need only reprint pages 7-8 (actually, vii-viii, i.e. the table of
contents) and pages 543-585 (last two pages of chapter 1, chapter 2, and
index).

Sorry about that.
Tom