[isabelle-dev] document_output vs. old document_dump/document_dump_mode

Lawrence Paulson lp15 at cam.ac.uk
Wed Aug 29 12:14:54 CEST 2012

This has always been my approach as well. Long ago I wrote a little script for post-processing the latex files.

On 29 Aug 2012, at 07:16, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:

> I use -D/document_dump extensively for producing papers. The Isabelle Latex output pretty much always requires post processing for anything that has higher type setting requirements. My standard setup these days is not to use root.tex for papers, but only to generate .tex from .thy, then post-process, then include manually in a master .tex file. 

More information about the isabelle-dev mailing list