[isabelle-dev] Looking up things (Re: Function Package questions)

[Makarius]

On Thu, 17 Apr 2008, Alexander Krauss wrote:

> Hi Moa,
> 
> I'm forwarding your questions to the isabelle-dev list, since they are 
> not actually Function Package questions, and more people might want to 
> comment on this.
> 
> > We're currently trying to get some information out about what's defined 
> > in a particular theory. Working on the ML level is it possible to:
> 
> > - Get the names of any functions/constants defined *by the user* in a 
> > given theory?

What exactly do you mean by *by the user*?  Even when you say ``definition 
"c = t"'' this is already a derived thing, as produced by the definition 
package.

Looking at the sources for the 'print_theory' command you will get an idea 
how to retrieve the internal logical entities currently available (types, 
consts, axioms in particular).

More recently we have started to make packages mark auxiliary definitions 
as "internal", so maybe this will help you here.  This status can be 
checked for theorems using PureThy.is_internal.


> So I'd like to know where your particular need arises for these things.

I would also like to know more.


	Makarius