[isabelle-dev] Looking up things (Re: Function Package questions)
makarius at sketis.net
Thu Apr 17 10:56:23 CEST 2008
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
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.
More information about the isabelle-dev