*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Theorem dependencies in jEdit*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 18 Dec 2014 11:47:42 +0100*In-reply-to*: <1418898250.1465.12.camel@kit.edu>*References*: <1418898250.1465.12.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.2.0

On 18.12.2014 11:24, Joachim Breitner wrote: > 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. There should be some newer code for that, written by Lukas Bulwahn and Rafal Kolanski about two years ago. IIRC it went into the Isabelle Cookbook. Have a look at the stuff around page 66 (in chapter 3.7 Theorems) There ought to be some newer code in the Isabelle Cookbook (generated from changeset 8d30446d89f0). > 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). As far as I understand, the default level of 0 already stores the references to named theorems, so there should be no need to enable more detailed proof terms. -- Lars

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Theorem dependencies in jEdit***From:*Joachim Breitner

**References**:**[isabelle] Theorem dependencies in jEdit***From:*Joachim Breitner

- Previous by Date: [isabelle] Theorem dependencies in jEdit
- Next by Date: Re: [isabelle] Theorem dependencies in jEdit
- Previous by Thread: [isabelle] Theorem dependencies in jEdit
- 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