[isabelle] Theorem dependencies in jEdit



Dear List,

in order to get a better handle on my formalizations I’d like to build
some tools, similar to unused_thms, that can aid guide my reorganization
of lemmas and theories. The data I need for that are the theory graph
and the lemma dependencies.

I found this code to extract the list of theorems used by a particular
theorem:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2006-March/msg00091.html
which I adjusted to today’s definition of PThm.


In that thread it is noted that "-p 1" has to be used. Is that
information still valid in 2014? I could not find a mention of this
option in the systems manual nor "isabelle jedit --help". Note that I do
not care about the dependencies on lemmas in the underlying heap (if
that makes a difference).

It seems that adding
        ML "Proofterm.proofs := 2"
to the top of my developments makes the code above actually do something
useful, but not ":= 1", which I presume corresponds to what "-p 1" used
to be. Is this mode "1" still supported?


Thanks,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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