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; Mon, 10 Oct 1994 19:31:51 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA27498; Mon, 10 Oct 1994 12:33:43 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA27488; Mon, 10 Oct 1994 12:33:33 -0600 Received: from switha.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Mon, 10 Oct 1994 18:35:05 +0100 To: Phil Windley Cc: hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Little things: "Draft mode" In-Reply-To: Your message of "Mon, 10 Oct 1994 11:14:44 MDT <9410101714.AA01120@jaguar.cs.byu.edu> Date: Mon, 10 Oct 1994 18:35:02 +0100 From: "Tom. F. Melham" Message-ID: <"swan.cl.cam.:262200:941010183218"@cl.cam.ac.uk> > What little things about HOL bother you? Draft mode vs non-draft mode. Its tiresome to teach, unnecessary, and messes up the implementation and documentation. We should abolish the distinction altogether and be in "draft mode" all the time. On the other point, I certainly wouldn't like new_theory to overwrite existing theories. But surely there's a consensus among the software engineers and HCI practicioners on such file-creating operations. Anyone know about this? Tom