Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Sat, 12 Dec 1992 09:32:14 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03832;
          Sat, 12 Dec 92 01:19:54 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA03827;
          Sat, 12 Dec 92 01:19:47 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA09323;
          Sat, 12 Dec 92 01:19:12 -0800
Message-Id: <9212120919.AA09323@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: hol-lcf and basic-hol
Date: Sat, 12 Dec 92 01:19:11 PST
From: chou@edu.ucla.cs

In the new HOL 2.01, after "make hol" is done, are hol-lcf and
basic-hol still needed?  I seem to recall that in version 2.00
"make hol" automatically zeros hol-lcf and basic-hol after
it's done.  Version 2.01 doesn't do that.

- Ching Tsun