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 Jul 1995 11:11:26 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA280840747; Mon, 10 Jul 1995 04:05:47 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from relay1.pipex.net by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA280810720; Mon, 10 Jul 1995 04:05:20 -0600 Received: from Q.icl.co.uk by flow.pipex.net with SMTP (PP); Mon, 10 Jul 1995 11:05:43 +0100 Received: from norman.win.icl.co.uk (norman.win01.icl.co.uk) by Q.icl.co.uk (4.1/icl-2.12-server) id AA07158; Mon, 10 Jul 95 11:04:53 BST From: Rob Arthan Date: Mon, 10 Jul 95 11:05:48 BST Message-Id: <9507101005.15408.0@win.icl.co.uk> To: slind@informatik.tu-muenchen.de Subject: Re: Theory signatures & remaking definitions in HOL Cc: hol2000@leopard.cs.byu.edu As Konrad thought, ProofPower does let the user delete definitions (and axioms). The mechanism isn't quite the same as Konrad's theorems which change colour when relevant definitions change. Theorems are marked with the name and "version number" of the theory which was current when they were proved. Theories are marked with a current version number and the set of version numbers which have been invalidated by deletions. When a theorem is inferred the system complains if the antecedents are marked with invalid version numbers. The run-time overhead is negligible in normal use, because the set of invalid version numbers is typically very small. The mechanism is not as liberal as one might like. Definitions have to be deleted in a last-in-first-to-go fashion. However, it's a great deal better than not being able to delete definitions at all. Rob Arthan (rda@win.icl.co.uk)