Re: [isabelle] thm dependencies



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.