Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu, schneide@ira.uka.de
Subject: Re: How do I get the definition of a constant in HOL90? 
In-Reply-To: Your message of "Tue, 06 Feb 1996 14:37:28 +0100."
             <"iraun1.ira.505:06.02.96.13.38.42"@ira.uka.de> 
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Tue, 06 Feb 1996 15:26:59 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <E0tjpIf-0006Pz-00@bescot.cl.cam.ac.uk>


Ralf writes:

> Given the name of a constant "X", how do I get the definition of that
> constant in HOL90 in a COMPUTABLE way? To be more precise, I want to
> have a sml-function "val foo : string -> thm", which takes the name
> of a constant "X" and returns the definitional theorem.
> 
> E.g. const_decl "X" does only give me the constant itself, its
> fixity and the theory, where it is defined. But I don't only want to know
> the theory, but the definition, too. Definitions can only retrieved by
> their own definition names, but there is no direct relation between
> the name of a constant and the name of the definition. There are
> unwritten conventions for naming the definition after the constants it
> defines, but that's only a convention and not a fact I can rely on.

You are right in thinking there is no way to do this in hol90.7.  It
would require only a minor modification to the system, and we shall
definitely consider it for the next version of hol90.

Cheers,
Don