Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 9 Nov 1992 04:46:22 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23661; Sun, 8 Nov 92 20:29:49 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from [130.56.4.1] by ted.cs.uidaho.edu (16.6/1.34) id AA23654; Sun, 8 Nov 92 20:29:30 -0800 Received: from mehta (mehta.anu.edu.au) by anu.anu.edu.au (4.1/SMI-4.1) id AA25813; Mon, 9 Nov 92 15:29:43 EST Received: by mehta (4.1/SMI-4.1) id AA24348; Mon, 9 Nov 92 15:32:25 EST Date: Mon, 9 Nov 92 15:32:25 EST From: symdchon@au.edu.anu.mehta (donald syme ) Message-Id: <9211090432.AA24348@mehta> To: info-hol@edu.uidaho.cs.ted Subject: Seperating theorems from definitions Cc: symdchon@mehta. This is just an idea, but has anyone thought of changing any of the existing versions of HOL so that the definitional parts of theories (axioms, constants, types, definitions) are stored in a seperate file to the theorems associated with the theory? My main reason for wanting this is due to the fact that I make extensive use of makefiles to automatically rebuild my theory heirarchy when I make some changes. The problem is that whenever I just add a theorem to a file, the timestamp gets updated and the whole theory heirarchy gets rebuilt. However, it would seem more logical (but perhaps harder to implement) to seperate these out. Of course, there are other fixes to the problem (like using versions of theHOL functions which adjust time stamps and/or signal updates by other means). Just wondering though. Donald Syme Australian National University.