How to: PDFs by Isabelle for the impatient ========================= Everything below in done inside a console (terminal), if you use Windows you might need to install such a program (e.g. cygwin, ming, ...). 1) Open console, go to directory where you .thy file is located > cd directory/to/theory/file We assume isabelle to be accessible in your PATH variable. If this is not the case, replace every occurrence of "isabelle" by the explicit qualified call to isabelle, e.g. "/home/alex/myisabelledirectory/bin/isabelle". 2) Create new Isabelle session using the 'isabelle' tool > isabelle mkroot -d This creates a ROOT file and some more stuff. 3) Open the ROOT file in a text editor, add your theory name to the "theories" section and save the file. It may now look like this (without the | signs of course). | session "resources" = "HOL" + | options [document = pdf, document_output = "output"] | theories [document = false] | (* Foo *) | (* Bar *) | theories | Example | document_files | "root.tex" 4) Build the document by > isabelle build -D . 5) If no build error (latex error) occurs, the PDF document can be found in ./output/document.pdf.