Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <14577-0@swan.cl.cam.ac.uk>; Tue, 18 Aug 1992 22:32:18 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13418; Tue, 18 Aug 92 14:20:28 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from dewdrop.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) id AA13412; Tue, 18 Aug 92 14:20:11 -0700 Received: by dewdrop.cs.ucdavis.edu (5.57/UCD.CS.2.0) id AA19214; Tue, 18 Aug 92 14:17:33 -0700 Message-Id: <9208182117.AA19214@dewdrop.cs.ucdavis.edu> To: David Shepherd Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list) Subject: Re: hol90 In-Reply-To: Your message of Tue, 18 Aug 92 10:49:45 +0100 Date: Tue, 18 Aug 92 14:17:30 -0700 From: kalvala@edu.ucdavis.cs X-Mts: smtp > From: David Shepherd > > is anyone using it? I've been using hol90 for several months, and have been quite pleased with it. Not very different from hol88, with the advantage Paul Loewenstein pointed out of allowing one to use SML. One warning I have is that the parsing of terms (especially of type information) is slightly different, and provides reduced error messages. Any plans to improve parsing, Konrad? - Sara