Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id QAA04279; Tue, 6 Feb 1996 16:59:29 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA027724053; Tue, 6 Feb 1996 06:40:53 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu with SMTP
	(1.37.109.15/16.2) id AA027383998; Tue, 6 Feb 1996 06:39:58 -0700
Received: from ira.uka.de (actually i80s11.ira.uka.de) by iraun1.ira.uka.de 
          with SMTP (PP); Tue, 6 Feb 1996 14:37:33 +0100
X-Mailer: exmh version 1.5.3 12/28/94
To: info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de, schneide@ira.uka.de
Subject: How do I get the definition of a constant in HOL90?
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 06 Feb 1996 14:37:28 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.505:06.02.96.13.38.42"@ira.uka.de>

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.

Ralf


(*********************************************************************)
(*                                                                   *)
(*  Ralf Reetz                                                       *)
(*  Research Assistent                                               *)
(*  Sonderforschungsbereich 358 der deutschen Forschungsgemeinschaft *)
(*  "Automatisierter Systementwurf"                                  *)
(*  University of Karlsruhe                                          *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                  *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany                *)
(*                                                                   *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de    *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html         *)
(*  fax:    +49 721 370455                                           *)
(*  tel:    +49 721 6084220                                          *)
(*                                                                   *)
(*********************************************************************)