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, 1 Nov 1994 16:34:24 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA23548; Tue, 1 Nov 1994 09:29:51 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from csg.uwaterloo.ca by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA23544; Tue, 1 Nov 1994 09:29:49 -0700 Received: by csg.uwaterloo.ca id <765>; Tue, 1 Nov 1994 11:24:00 -0500 Subject: Re: bhogan@bedlam: HOL90 on a PC From: Peter Bumbulis To: info-hol@leopard.cs.byu.edu Date: Tue, 1 Nov 1994 11:23:58 -0500 X-Mailer: ELM [version 2.3 PL11] Message-Id: <94Nov1.112400est.765@csg.uwaterloo.ca> Another option for HOL on a PC is to use gcl (available from math.utexas.edu in pub/gcl; compiles without problems under Linux) and hol88 2.02: hol88 compiles without problem using gcl. hol88 seems to perform better on my (Linux) system than hol90.6; I suspect that this is due to the fact that I have a limited amount of memory. Peter