Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <09526-0@swan.cl.cam.ac.uk>; Tue, 18 Aug 1992 17:08:30 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11527; Tue, 18 Aug 92 08:42:35 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA11522; Tue, 18 Aug 92 08:42:15 -0700 Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) id AA03273; Tue, 18 Aug 92 08:40:42 PDT Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA08365; Tue, 18 Aug 92 08:40:43 PDT Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA01338; Tue, 18 Aug 92 08:41:59 PDT Date: Tue, 18 Aug 92 08:41:59 PDT From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein) Message-Id: <9208181541.AA01338@lara.Eng.Sun.COM> To: des@uk.co.inmos, info-hol@edu.uidaho.cs.ted In-Reply-To: David Shepherd's message of Tue, 18 Aug 92 10:49:45 BST <20158.9208180949@frogland.inmos.co.uk> Subject: hol90 I have been using it for some time. It appears to work fine. Some minor differences, including some operator precedences. More memory hungry than HOL88. Library loading is a bit painful (top level bindings have to introduced by generating scripts and reading them; no hacking of the ML system as in HOL88.). I changed because I wanted to code some more elaborate proof procedures, and wanted to use a live language and Paulson's book. Paul Loewenstein -- paul.loewenstein@Eng.sun.com Staff Engineer, Sun Microsystems