Re: [isabelle] theory file info



Hi Sean,

>   Is there a way to find out which types/constants/axioms are  defined
> *just* within
> a particular theory?  My (partial) understanding is as follows,
> Sign.req_sg, Type.rep_tsig, etc gives you full information
> about the types etc. that are currently in scope.  So, the info
> from, say,
> Sign.rep_sg (theory "HOL")
> are a subset of those of
> Sign.rep_sg (theory "Set")

This understanding is sufficently right (the term "scope" is misleading
in this context, but that does not matter for the particular problem).

> Is there an easy way, without looking at the theory file itself, to get
> just the types etc. defined in, say, Set.thy?

Not a direct way, but you can achieve that by enumerating all constants
 (type constructors, ...) in the current theory and from that set taking
away all constants  (type constructors, ...) present in the ancestor
theories (see Theory.parents_of).

To get an idea how this may work, have a look at src/Pure/codegen.ML,
functions theory_of_const and thyname_of_const which show how this could
work in principle.

Hope this helps
Florian

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.