*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] thm dependencies*From*: John Matthews <matthews at galois.com>*Date*: Tue, 25 Oct 2005 09:11:25 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.58.0510251615530.7555@atbroy65.informatik.tu-muenchen.de>*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> <Pine.LNX.4.58.0510251615530.7555@atbroy65.informatik.tu-muenchen.de>

text {* Extract the abstract syntax of a theorem's oracle tags. *} ML {* fun oracle_terms_of_thm thm = Proofterm.oracles_of_proof [] (proof_of thm) *}

ML {* fun oracle_strings_of_thm thm = let val thy = theory_of_thm thm

(oracles_of_thm thm) end *} -john On Oct 25, 2005, at 7:19 AM, Makarius wrote:

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 storedwithinthe "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 entrieslikethis: fn G => Graph.all_succs G (Graph.minimals G) Makarius

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

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

**Re: [isabelle] thm dependencies***From:*Makarius

- 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