[isabelle] theory file info



Hello,

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")

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

The reason I'd like this info is that I'd like to do the translation to
HOL Light by theory, rather than all at once.  Knowing what is
defined in which theory would make this possible.

Thanks,

Sean





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