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, 15 Mar 1994 00:30:12 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA29543; Mon, 14 Mar 1994 17:15:31 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA29536; Mon, 14 Mar 1994 17:15:07 -0700 Received: from itd0.dsto.gov.au by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA28188; Mon, 14 Mar 1994 16:15:01 -0800 Received: from tcs22.dsto.gov.au by itd0.dsto.gov.au with SMTP (5.64+1.3.1+0.50/DSTO-1.0) id AA06719; Tue, 15 Mar 1994 10:43:17 +1030 Date: Tue, 15 Mar 1994 10:43:17 +1030 From: Jim Grundy Message-Id: <9403150013.AA06719@itd0.dsto.gov.au> To: info-hol@cs.uidaho.edu Subject: Re: [Konrad Slind: question about HOL90] Konrad writes: > The decision to adopt records was made without consulting the HOL > community, a point that has been made to me many times (usually by John > Harrison). It seems that a reasonable time has passed for people to > decide if they like them. So: what do people think? Well I think John is right. I am in the middle of porting my window library to HOL90. I think this change, while well intentioned, and perhaps more in line with the SML philosophy of life, doesn't really give me anything I didn't have before and brings with it a lot of hassle for people doing ports. It also moves HOL90 further away from HOL88 which is not such a good thing given the lack of HOL90's own documentation. The only thing that stops me saying "change it back" is the knowledge that I would then have to re-edit all my files again. The world would be a nicer place if there was just one HOL. Probably that HOL should be HOL90. Making alterations like this one, won't encourage people to make the switch. Jim