# [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.*