Re: [isabelle] Excluding theories from the session_graph output



On Mon, 28 Apr 2014, Joachim Breitner wrote:

Hello Makarius,

Am Montag, den 28.04.2014, 20:24 +0200 schrieb Makarius:
For now I recommend to let the system do its work with minimal
intervention.  E.g. what is the purpose of the Everything.thy instead of
just listing all its imports in ROOT?

it not only imports everything, but also contains TeX code with anti-quotations that state the main results. See http://afp.sourceforge.net/browser_info/current/AFP/Launchbury/document.pdf where section 1.1 is the result of Isabelle processing Everything.thy.

I would say that small imperfection is OK. If/when some reform of the graph presentation tool happens eventually, you should remind the person who does it to provide some simple means to filter the result.


	Makarius




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