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 08:06:11 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02258; Tue, 15 Mar 1994 00:51:04 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA02254; Tue, 15 Mar 1994 00:50:57 -0700 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Tue, 15 Mar 1994 08:46:01 +0000 Received: from ira.uka.de by i80fs2.ira.uka.de id <09494-0@i80fs2.ira.uka.de>; Tue, 15 Mar 1994 08:50:54 +0100 Date: Tue, 15 Mar 94 8:50:53 EST From: reetz To: info-hol@leopard.cs.byu.edu Subject: RE: HOL90 - Syntax Message-Id: <"i80fs2.ira.496:15.02.94.07.50.59"@ira.uka.de> 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? IMHO it is not a big thing. Adapting to the new "syntax" was'nt a big deal, just a boring one. IMHO, it's a question of taste: reading #conseq is somewhat nicer than snd . Furthermore, my students found it easier to remember. As Jim Grundy has noted, changing back would be just another boring work to do I really wouldn't like to. :) Ralf (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)