[isabelle] Theorem dependencies



When generating the graph of theorem dependencies for a non-trivial theorem in a
quite large theory, one usually does not want to see all of his/her theorems
there.  A concrete example: one may have a group of ten related minor lemmata
that are used in the proof of a large theorem.  It would be nice if these ten
could be "grouped" together as a single node in the dependency graph.

At the moment, the only way I know to achieve this effect is to put the ten
lemmata in a separate theory.  Wouldn't it be nice if the dependency graph could
 understand, for example, the sectioning mechanism?  Has anyone tried to do what
I suggest?  Or have a different workaround?

Thanks,
Nikos.

-- 
Nikolaos S. Papaspyrou, Assistant Professor | Tel:  +30-210-7723393, fax: 2519
National Technical University of Athens     | Home: +30-210-7524801
School of Electrical & Computer Engineering |----------------------------------
Software Engineering Laboratory             | E-mail: nickie at softlab.ntua.gr
15780 Zografou, Athens, Greece              | URL: www.softlab.ntua.gr/~nickie/





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