src/Doc/System/Presentation.thy
changeset 52744 49825ba687ce
parent 51417 d266f9329368
child 52746 eec610972763
equal deleted inserted replaced
52743:a7d69a11f395 52744:49825ba687ce
   286   Appropriate {\LaTeX}-related programs are run on the input file,
   286   Appropriate {\LaTeX}-related programs are run on the input file,
   287   according to the given output format: @{executable latex},
   287   according to the given output format: @{executable latex},
   288   @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
   288   @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
   289   (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
   289   (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
   290   idx}).  The actual commands are determined from the settings
   290   idx}).  The actual commands are determined from the settings
   291   environment (@{setting ISABELLE_LATEX} etc.).
   291   environment (@{setting ISABELLE_PDFLATEX} etc.).
   292 
   292 
   293   The @{verbatim sty} output format causes the Isabelle style files to
   293   The @{verbatim sty} output format causes the Isabelle style files to
   294   be updated from the distribution.  This is useful in special
   294   be updated from the distribution.  This is useful in special
   295   situations where the document sources are to be processed another
   295   situations where the document sources are to be processed another
   296   time by separate tools.
   296   time by separate tools.