src/Doc/System/Presentation.thy

 \<open>Usage: isabelle document [OPTIONS]
 
   Options are:
     -d DIR       document output directory (default "output/document")
     -n NAME      document name (default "document")
-    -o FORMAT    document format: pdf (default), dvi
     -t TAGS      markup for tagged regions
 
   Prepare the theory session document in document directory, producing the
   specified output format.
 \<close>}

   Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   will appear in the parent of this directory.
 
   \<^medskip>
-  The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
-  the default is ``\<^verbatim>\<open>document.pdf\<close>''.
+  Option \<^verbatim>\<open>-n\<close> specifies the resulting document file name, the default is
+  ``\<^verbatim>\<open>document\<close>'' (leading to ``\<^verbatim>\<open>document.pdf\<close>'').
 
   \<^medskip>
   The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
   regions. Tags are specified as a comma separated list of modifier/name
   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to

   \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
   of predefined Isabelle symbols. Users may invent further symbols as well,
   just by providing {\LaTeX} macros in a similar fashion as in
   \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
 
-  For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
+  For proper setup of PDF documents (with hyperlinks and bookmarks),
   we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
 
   \<^medskip>
   As a final step of Isabelle document preparation, @{tool document} is run on
   the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document

   document preparation. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle latex [OPTIONS] [FILE]
 
   Options are:
-    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty
+    -o FORMAT    specify output format: pdf (default), bbl, idx, sty
 
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.\<close>}
 
   Appropriate {\LaTeX}-related programs are run on the input file, according
-  to the given output format: @{executable latex}, @{executable pdflatex},
-  @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
-  makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
-  settings environment (@{setting ISABELLE_PDFLATEX} etc.).
+  to the given output format: @{executable pdflatex}, @{executable bibtex}
+  (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands
+  are determined from the settings environment (@{setting ISABELLE_PDFLATEX}
+  etc.).
 
   The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
   the distribution. This is useful in special situations where the document
   sources are to be processed another time by separate tools.
 \<close>