*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Document preparation question*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 17 Jan 2013 11:36:36 +0100*In-reply-to*: <50F7D098.50204@inf.ethz.ch>*References*: <1358414370.4392.23.camel@kirk> <50F7D098.50204@inf.ethz.ch>

Hi, Am Donnerstag, den 17.01.2013, 11:21 +0100 schrieb Andreas Lochbihler: > > Also, I have trouble with no_document. My ROOT.ML reads > > $ cat isa-launchbury/ROOT.ML > > no_document use_thys ["~~/src/HOL/Library/FuncSet", "~~/src/HOL/Library/LaTeXsugar"]; > > use_thys ["Everything"]; > > And indeed, the generated files FuncSet.tex and LaTeXsugar.tex are > > empty. But they are included in the session_graph.pdf file. Is there a > > way to avoid that? > I know one way to avoid that: Build a heap image with all auxiliary > theories that you do not want to show up in session_graph.pdf, i.e., HOL > with FuncSet and LaTeXsugar, and then base your session on this image. Or, in my case, HOL+HOLCF+Nominal2+FuncSet+LaTeXsugar. This leads to another question: What should a IsaMakefile look like that uses a custom heap (in my case, HOL+HOLCF+Nominal2 where Nominal2 comes with my submission in a subdirectory) so that it works on the AFP? Also, one of the theories that I want to exclude from the session graph is Everything, which is actually the part of the introduction that uses all this pretty-printing, but not really part of the theory. I guess the heap building does not work here, because the theory is at the very bottom of the graph? > > I also miss good ways to automatically print data type definitions. My > > work around is to show > > lemma Terms: > > "∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))" > > by (metis Terms.exp_assn.exhaust(1)) > > and pretty-print this lemma in the text, but a tool that formats an > > exhaust-lemma in the style of a grammar specification would be slick. > You don't have to state and prove this lemma yourself, the datatype > package generates a similar one called expr.nchotomy for type expr. Thanks for the pointer. It seems that nominal_datatye does not build such a lemma. Also, I had to collect all existentially quantified variables in the front so that the lemma would fit on one line :-) Greetings, Joachin -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] Document preparation question***From:*Joachim Breitner

**Re: [isabelle] Document preparation question***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Document preparation question
- Next by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Previous by Thread: Re: [isabelle] Document preparation question
- Next by Thread: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list