Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 22 Jun 1993 05:11:41 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04109;
          Mon, 21 Jun 93 20:57:16 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA04104;
          Mon, 21 Jun 93 20:57:12 -0700
Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) 
          id AA09989; Mon, 21 Jun 93 20:57:36 PDT
Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA25274;
          Mon, 21 Jun 93 20:57:42 PDT
Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA04736;
          Mon, 21 Jun 93 21:01:23 PDT
Date: Mon, 21 Jun 93 21:01:23 PDT
From: Paul.Loewenstein@Eng.Sun.COM (Paul Loewenstein)
Message-Id: <9306220401.AA04736@lara.Eng.Sun.COM>
To: info-hol@ted.cs.uidaho.edu
Subject: HOL90 is faster, for me
In-Reply-To: Malcolm Newey's message of Mon, 21 Jun 1993 12:34:27 +1000 <199306210234.AA03906@achernar.anu.edu.au>




It is not just speed that should dictate as rapid as possible move to HOL90.

It is quite clear that more sophisticated proof procedures are required
(and are being added) to reduce unnecessarily tedious human interaction.

Why make all this programming effort in a dead language?

I would love to see more encouragement to make the switch, possibly
by a policy of introducing significant new features and proof procedures
to HOL90 first.

The sooner we all move, the less total work there will be doing it.

         Paul.