Re: [isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients?



On Thu, 31 Oct 2013, Gottfried Barrow wrote:

There are no PDF documents for the new HOL-BNF sessions at this site:

http://isabelle.in.tum.de/website-Isabelle2013-1-RC3/dist/library/HOL/index.html

This is simply because HOL-BNF does not provide a document. There is no obligations for Isabelle sessions to include such documents. The BNF guys do provide a separate manual "datatypes".


I'm not set up to build any PDFs on my machine, and there would probably be failures if I tried.

It should work after running the batch file Isabelle2013-1-RC3\Cygwin-Latex-Setup and waiting patiently untile approx. 500 MB disk space is filled up.

Then you can produce session documents like this (via Cygwin-Terminal):

  isabelle build -o browser_info -o document=pdf -v HOL-Library

For already built sessions without generated document, you might need option -c as well.


	Makarius




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