*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Theorem dependencies in jEdit*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 18 Dec 2014 11:24:10 +0100

Dear List, in order to get a better handle on my formalizations I’d like to build some tools, similar to unused_thms, that can aid guide my reorganization of lemmas and theories. The data I need for that are the theory graph and the lemma dependencies. I found this code to extract the list of theorems used by a particular theorem: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2006-March/msg00091.html which I adjusted to today’s definition of PThm. In that thread it is noted that "-p 1" has to be used. Is that information still valid in 2014? I could not find a mention of this option in the systems manual nor "isabelle jedit --help". Note that I do not care about the dependencies on lemmas in the underlying heap (if that makes a difference). It seems that adding ML "Proofterm.proofs := 2" to the top of my developments makes the code above actually do something useful, but not ":= 1", which I presume corresponds to what "-p 1" used to be. Is this mode "1" still supported? Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Theorem dependencies in jEdit***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Scala codegen error: need NatO, natT, and NatC
- Next by Date: Re: [isabelle] Theorem dependencies in jEdit
- Previous by Thread: Re: [isabelle] Scala codegen error: need NatO, natT, and NatC
- Next by Thread: Re: [isabelle] Theorem dependencies in jEdit
- Cl-isabelle-users December 2014 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