Re: [isabelle] Theorem dependencies in jEdit



On 18.12.2014 11:24, Joachim Breitner wrote:
> 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.

There should be some newer code for that, written by Lukas Bulwahn and
Rafal Kolanski about two years ago. IIRC it went into the Isabelle Cookbook.

Have a look at the stuff around page 66 (in chapter 3.7 Theorems)
There ought to be some newer code in the Isabelle Cookbook (generated
from changeset 8d30446d89f0).

> 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).

As far as I understand, the default level of 0 already stores the
references to named theorems, so there should be no need to enable more
detailed proof terms.

  -- Lars

Attachment: signature.asc
Description: OpenPGP digital signature



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