*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] thm dependencies*From*: Makarius <makarius at sketis.net>*Date*: Tue, 25 Oct 2005 16:19:23 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <ed33c84c18e7931f93418789b356b80d@galois.com>*References*: <000001c5d5f0$925134f0$8705e29f@ios.ac.cn> <4358B666.1090306@loria.fr> <46B0A3C8-BD59-49F7-804B-A9223B84E902@cmu.edu> <Pine.LNX.4.58.0510241408380.14074@atbroy65.informatik.tu-muenchen.de> <0A1281DA-7255-4D42-A662-57C4612A30F6@cmu.edu> <ed33c84c18e7931f93418789b356b80d@galois.com>

On Tue, 25 Oct 2005, John Matthews wrote: > Similarly, how to I extract the list of external oracles used in the > proof of a tagged theorem, when theorem dependencies are turned off? See Pure/proofterm.ML for some operations on proof terms as stored within the "der" field of a thm. > On Oct 24, 2005, at 5:52 PM, Sean McLaughlin wrote: > > I'd like a way to extract the theorem dependencies of a theorem. I > > know Isabelle has a great facility for plotting these deps with > > "thm_deps", but is there a way to just extract a tree of dependencies > > (that could be topologically sorted, say). See Pure/Thy/thm_deps.ML. You may build a Graph.T (cf. Pure/General/graph.ML) and get a toplogically sorted list of entries like this: fn G => Graph.all_succs G (Graph.minimals G) Makarius

**Follow-Ups**:**Re: [isabelle] thm dependencies***From:*John Matthews

**References**:**[isabelle] TLA thoery in src directory***From:*yongjian Li

**Re: [isabelle] TLA thoery in src directory***From:*Stephan Merz

**[isabelle] term_tvars***From:*Sean McLaughlin

**[isabelle] thm dependencies***From:*Sean McLaughlin

**Re: [isabelle] thm dependencies***From:*John Matthews

- Previous by Date: Re: [isabelle] thm dependencies
- Next by Date: Re: [isabelle] thm dependencies
- Previous by Thread: Re: [isabelle] thm dependencies
- Next by Thread: Re: [isabelle] thm dependencies
- Cl-isabelle-users October 2005 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