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; Thu, 20 Oct 1994 16:28:38 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA20276; Thu, 20 Oct 1994 09:25:20 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA20264; Thu, 20 Oct 1994 09:24:59 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 20 Oct 1994 16:17:30 +0100 To: hol2000@leopard.cs.byu.edu Subject: Re: Little things: "Draft mode" In-Reply-To: Your message of "Mon, 10 Oct 94 18:35:02 BST." <"swan.cl.cam.:262200:941010183218"@cl.cam.ac.uk> Date: Thu, 20 Oct 94 16:17:18 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:034820:941020151747"@cl.cam.ac.uk> > What little things about HOL bother you? The mixing up of the parser with the rest of the system. In particular, all definition mechanisms are complicated by extra arguments for fixity etc, and when parsing the definition, the special status is unavailable, making the definition less readable. The distinction between constants and variables as far as special parse status is concerned merely decreases flexibility for no advantage (one often wants `local constants' in abstract theories). The right way is to have separate parser directives which apply to all identifiers. Theory files in general. They're an ugly hack which messes up the cleanliness of the LCF ideal and creates complications (again, extra arguments for names to store theorem under) and insecurity. I suppose something of the sort is a practical necessity, though. What is the opinion of Lambda and Isabelle people about relying on Poly-ML's persistent storage? How about just saving differential ML images? For more on these issues see the Category B paper Konrad and I wrote for HUG94. John.