Re: [isabelle] Excluding theories from the session_graph output



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.

> Suppressing LaTeXsugar.thy could work by an auxiliary base session, 
> although for the purpose of AFP that is probably a bit much extra weight. 
> Since LaTeXsigar is part of the HOL-Library session, you could use that as 
> a base if you don't have any other special one already.

Basing my HOLCF+Nominal2 session (which is the base for my work) on
HOL-Library is a good idea to solve that, thanks!

Greetings,
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.