*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] theory file info*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Tue, 07 Feb 2006 10:54:06 +0100*In-reply-to*: <0E2E28A8-5F06-4D11-9B69-6C51B804849A@cmu.edu>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <0E2E28A8-5F06-4D11-9B69-6C51B804849A@cmu.edu>*User-agent*: Mozilla Thunderbird 1.0 (Windows/20041206)

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**

**References**:**[isabelle] theory file info***From:*Sean McLaughlin

- Previous by Date: [isabelle] theory file info
- Next by Date: [isabelle] square root
- Previous by Thread: [isabelle] theory file info
- Next by Thread: [isabelle] square root
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list