[isabelle] theory file info
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and