*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Theorem dependencies in jEdit*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 18 Dec 2014 13:46:34 +0100*In-reply-to*: <5492B0CE.3090600@in.tum.de>*References*: <1418898250.1465.12.camel@kit.edu> <5492B0CE.3090600@in.tum.de>

Hi Lars, Am Donnerstag, den 18.12.2014, 11:47 +0100 schrieb Lars Noschinski: > On 18.12.2014 11:24, Joachim Breitner wrote: > 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). thanks for the pointer. I often forget about the Cookboook. Is there a good reason it is not included with the other documentation that comes with Isabelle? Based on the information there I came up with this code that traverses the tree of used theorems, stopping at those that have a name: fun thms_used_by_thm thm = let fun used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> map go |> List.concat and go ("", _, pbodyf) = pbodyf |> Future.join |> used_by_proof_body | go (s, _, _) = [s] in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body end; > 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. Indeed, thanks! Greetings, 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:*Makarius

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

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

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