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
fn G => Graph.all_succs G (Graph.minimals G)
This archive was generated by a fusion of
Pipermail (Mailman edition) and