1.1 --- a/doc-src/System/present.tex	Thu May 15 18:12:43 2008 +0200
     1.2 +++ b/doc-src/System/present.tex	Thu May 15 20:02:37 2008 +0200
     1.3 @@ -579,9 +579,9 @@
     1.4  {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the
     1.5  distribution.
     1.6  
     1.7 -For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
     1.8 -images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
     1.9 -do so even without using PDF~\LaTeX.
    1.10 +For proper setup of PDF documents (with hyperlinks and bookmarks), we
    1.11 +recommend to include \verb,pdfsetup.sty, as well.  It is safe to do so
    1.12 +even without using PDF~\LaTeX.
    1.13  
    1.14  \medskip As a final step of document preparation within Isabelle,
    1.15  \texttt{isatool document -c} is run on the resulting \texttt{document}
    1.16 @@ -604,16 +604,17 @@
    1.17  
    1.18    Options are:
    1.19      -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
    1.20 -                 ps.gz, pdf, bbl, png, sty, syms
    1.21 +                 ps.gz, pdf, bbl, idx, sty, syms
    1.22  
    1.23    Run LaTeX (and related tools) on FILE (default root.tex),
    1.24    producing the specified output format.
    1.25  \end{ttbox}
    1.26 -Appropriate {\LaTeX}-related programs are run on the input file, according to
    1.27 -the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
    1.28 -\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
    1.29 -The actual commands are determined from the settings environment
    1.30 -(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
    1.31 +Appropriate {\LaTeX}-related programs are run on the input file,
    1.32 +according to the given output format: \texttt{latex},
    1.33 +\texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}),
    1.34 +and \texttt{makeindex} (for \texttt{idx}).  The actual commands are
    1.35 +determined from the settings environment (\texttt{ISABELLE_LATEX}
    1.36 +etc., see \S\ref{sec:settings}).
    1.37  
    1.38  The \texttt{sty} output format causes the Isabelle style files to be updated
    1.39  from the distribution.  This is useful in special situations where the