Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Fri, 22 Jan 1993 00:00:11 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20216; Thu, 21 Jan 93 15:31:49 -0800 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 AA20211; Thu, 21 Jan 93 15:31:34 -0800 Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) id AA23081; Thu, 21 Jan 93 15:30:02 PST Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA15920; Thu, 21 Jan 93 15:30:16 PST Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA03970; Thu, 21 Jan 93 15:32:32 PST Date: Thu, 21 Jan 93 15:32:32 PST From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein) Message-Id: <9301212332.AA03970@lara.Eng.Sun.COM> To: chou@edu.ucla.cs In-Reply-To: chou@cs.ucla.edu's message of Thu, 21 Jan 93 14:33:54 PST <9301212233.AA10731@maui.cs.ucla.edu> Cc: info-hol@edu.uidaho.cs.ted Subject: Conversion from HOL88 to HOL90 Content-Length: 610 Converting from HOL88v2.x (in my case x=0) to HOL90 was usually straightforward. Usually only minor changes after hacking the syntax with emacs. The main difference being the lack of autoloading. I complicated things somewhat by choosing to explicitly load theorems as they are used. Converting from HOL88v1.x can be less straightforward, because of the different behaviour of the resolution tactics. Presumably this is also a problem upgrading to HOL88v2.x. (I think I have the HOL88 version numbers right). Paul Loewenstein -- paul.loewenstein@Eng.sun.com Staff Engineer, Sun Microsystems