Re: [isabelle] Document preparation question


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 :-)


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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