Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 21 Apr 1993 19:10:51 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20604; Wed, 21 Apr 93 11:00:56 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20599; Wed, 21 Apr 93 11:00:43 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 21 Apr 1993 19:00:12 +0100 To: David Shepherd Cc: info-hol@ted.cs.uidaho.edu (info-hol mailing list), Tom.Melham@cl.cam.ac.uk Subject: Re: Suggested additions to definition functions In-Reply-To: Your message of Wed, 21 Apr 93 12:48:53 +0100. <19533.9304211148@frogland.inmos.co.uk> Date: Wed, 21 Apr 93 19:00:03 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:081830:930421180018"@cl.cam.ac.uk> David Shepherd writes: > ...one problem - the underlying define_type mechanism > leaves a large number of definitions in the theory file that > never get used. > > ... make the definition (i.e. declare the relevant constant(s)), return > the theorem but not store it in the theory file. > > What does anyone think about these ideas? Well, I think we've got to be careful to retain a clean logical "story" --- so it's not just a software engineering issue. The logically-justified solution I've had in mind for a while now is the type specification rule discussed in the manual (or, rather, a combined constant/type specification rule). This would allow exactly what David wants - namely storing only the final property. Alas, however, if you start trying to use it in this way, you'll soon run up against the problem discussed in my paper at the last HOL user meeting... Tom