Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ppsw1.cam.ac.uk (actually pp@gray.csi.cam.ac.uk (mailer)) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cam;
          Mon, 10 Oct 1994 19:08:35 +0100
Received: from leopard.cs.byu.edu by ppsw1.cam.ac.uk 
          with SMTP-INT (PP-6.0) as ppsw.cam.ac.uk 
          id <08106-0@ppsw1.cam.ac.uk>; Mon, 10 Oct 1994 18:21:46 +0100
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA26176;
          Mon, 10 Oct 1994 11:19:40 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA26172;
          Mon, 10 Oct 1994 11:19:38 -0600
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA01120;
          Mon, 10 Oct 1994 11:14:45 -0600
Message-Id: <9410101714.AA01120@jaguar.cs.byu.edu>
To: hol2000@leopard.cs.byu.edu
Subject: little things that make HOL unfriendly....
Date: Mon, 10 Oct 1994 11:14:44 -0600
From: Phil Windley <windley@lal.cs.byu.edu>


This may not be something for HOL 2000, it may be something more suited for
HOL96, but...

One thing that bothers me is that new_theory won't overwrite an existing
theory file.  So, most of us regularly do:

system `/bin/rm -f theory.th`;;

new_theory `theory.th`;;

Once you know it, its not bad, but teaching it to beginners is just one
more nitpicky detail that they have to know.  This one small change is not
going to make HOL significantly better, but lots of them would.  

What little things about HOL bother you?  

--phil--