
diff -r 52e4de17734e -r f9d3c92eae4d doc-src/System/present.tex
--- a/doc-src/System/present.tex	Tue Dec 11 15:04:17 2001 +0100
+++ b/doc-src/System/present.tex	Tue Dec 11 15:36:28 2001 +0100
@@ -6,21 +6,40 @@
 Isabelle provides several ways to present the outcome of formal developments,
 including WWW-based browsable libraries or actual printable documents.
 Presentation is centered around the concept of \emph{logic sessions}.  The
-global session structure is that of a tree, with Isabelle \texttt{Pure} at its
-root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL},
-and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
-positions.  The latter usually do not have a separate {\ML} image.
+global session structure is that of a tree, with Isabelle Pure at its root,
+further object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
+application sessions in leaf positions (usually without a separate image).
 
 The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see
 \S\ref{sec:tool-make}) tools of Isabelle provide the primary means for
 managing Isabelle sessions, including proper setup for presentation.  Here the
-\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to run any
-additional stages required for document preparation, notably the tools
-\texttt{document} (see \S\ref{sec:tool-document}) and \texttt{latex} (see
-\S\ref{sec:tool-latex}).
+\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the
+\texttt{isabelle} process run any additional stages required for document
+preparation, notably the tools \texttt{document} (see
+\S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}).
+The complete tool chain for managing batch-mode Isabelle sessions is
+illustrated in figure~\ref{fig:session-tools}.
+
+\begin{figure}[htbp]
+  \begin{center}
+    \begin{tabular}{lp{0.6\textwidth}}
+      \texttt{isatool mkdir} & invoked once by the user to create the initial
+        source setup (common \texttt{IsaMakefile} plus a single session directory); \\
+      \texttt{isatool make} & invoked repeatedly by the user to
+        keep session output up-to-date (HTML, documents etc.); \\
+      \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\
+      \texttt{isabelle} & run through \texttt{isatool usedir}; \\
+      \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\
+      \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times
+        by \texttt{isatool document}; also useful for manual experiments; \\
+    \end{tabular}
+    \caption{The tool chain of Isabelle session presentation}
+    \label{fig:session-tools}
+  \end{center}
+\end{figure}
 
 
-\section{Generating theory browsing information} \label{sec:info}
+\section{Generating theory browser information} \label{sec:info}
 \index{theory browsing information|bold}
 
 As a side-effect of running a logic sessions, Isabelle is able to generate
@@ -34,36 +53,44 @@
 Isabelle also generates graph files that represent the theory hierarchy of a
 logic.  There is a graph browser Java applet embedded in the generated HTML
 pages, and also a stand-alone application that allows browsing theory graphs
-without having to start a WWW browser first.  The latter version also includes
+without having to start a WWW client first.  The latter version also includes
 features such as generating Postscript files, which are not available in the
 applet version.  See \S\ref{sec:browse} for further information.
 
 \medskip
 
-In order to let Isabelle generate theory browsing information, simply append
-``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
-making a logic.  For example, in order to do this for FOL, add this to your
-Isabelle settings file
+The easiest way to let Isabelle generate theory browsing information for
+existing sessions is to append ``\texttt{-i true}'' to the
+\settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or
+\texttt{./build} in the distribution).  For example, add something like this
+to your Isabelle settings file
 \begin{ttbox}
 ISABELLE_USEDIR_OPTIONS="-i true"
 \end{ttbox}
 and then change into the \texttt{src/FOL} directory of the Isabelle
 distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
+The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL},
+which usually refers to \verb,~/isabelle/browser_info/FOL,.  Note that option
+\texttt{-v true} will make the internal runs of \texttt{usedir} more explicit
+about such details.
 
-Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
+Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual
 printable documents.  These are prepared automatically as well if enabled like
 this, using the \texttt{-d} option
 \begin{ttbox}
 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
 \end{ttbox}
-See \S\ref{sec:tool-document} for further information on Isabelle document
-preparation.
+Enabling options \texttt{-i} and \texttt{-d} simultaneausly as shown above
+causes an appropriate ``document'' link to be included in the HTML index.
+Documents (or raw document sources) may be generated independently of browser
+information as well, see \S\ref{sec:tool-document} for further details.
 
-\bigskip The theory browsing information is stored within the directory
-determined by the \settdx{ISABELLE_BROWSER_INFO} setting.  The
-\texttt{index.html} file located there provides an entry point to all standard
-Isabelle logics.  A complete HTML version of all object-logics and examples of
-the Isabelle distribution is available at
+\bigskip The theory browsing information is stored in a sub-directory
+directory determined by the \settdx{ISABELLE_BROWSER_INFO} setting plus a
+prefix corresponding to the session identifier (according to the tree
+structure of sub-sessions by default).  A complete WWW view of all standard
+object-logics and examples of the Isabelle distribution is available at the
+Cambridge or Munich Isabelle sites:
 \begin{center}\small
   \begin{tabular}{l}
     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
@@ -71,31 +98,19 @@
   \end{tabular}
 \end{center}
 
-\medskip
-
-The generated HTML document of any theory includes all theorems proved in the
-corresponding {\ML} file, provided these have been stored properly via
-\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},
-\ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}).
-Section headings may be included in the presentation via the {\ML} function
-\begin{ttbox}\index{*section}
-section: string -> unit
-\end{ttbox}
-
-\medskip
-
-In order to present your own theories on the web, simply copy the
+\medskip In order to present your own theories on the web, simply copy the
 corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW
-server, after having generated browser info like this:
+server, having generated browser info like this:
 \begin{ttbox}
 isatool usedir -i true HOL Foo
 \end{ttbox}
 This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
-to load all your theories, and HOL is your parent logic image.  Ideally,
-theory browser information would have been generated for HOL already.
-
-Alternatively, one may specify an external link to an existing body of HTML
-data by giving \texttt{usedir} a \texttt{-P} option like this:
+to load all your theories, and HOL is your parent logic image (\texttt{isatool
+  mkdir} assists in setting up Isabelle session directories, see
+\S\ref{sec:tool-mkdir}).  Theory browser information for HOL should have been
+generated already beforehand.  Alternatively, one may specify an external link
+to an existing body of HTML data by giving \texttt{usedir} a \texttt{-P}
+option like this:
 \begin{ttbox}
 isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
 \end{ttbox}
@@ -105,8 +120,7 @@
 There is a separate \texttt{mkdir} tool to provide easy setup of all this,
 with only minimal manual editing required.
 \begin{ttbox}
-isatool mkdir Foo
-isatool make
+isatool mkdir HOL Foo && isatool make
 \end{ttbox}
 See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session
 directories, including the setup for documents.
@@ -115,11 +129,14 @@
 \section{Browsing theory graphs} \label{sec:browse}
 \index{theory graph browser|bold} 
 
-The graph browser is a tool for visualizing dependency graphs. Certain nodes
-of the graph (i.e.~theories) can be grouped together in ``directories'', whose
-contents may be hidden, thus enabling the user to filter out irrelevant
-information.  The browser is written in Java, it can be used both as a
-stand-alone application and as an applet.
+The Isabelle graph browser is a general tool for visualizing dependency
+graphs.  Certain nodes of the graph (i.e.~theories) can be grouped together in
+``directories'', whose contents may be hidden, thus enabling the user to
+collapse irrelevant portions of information.  The browser is written in Java,
+it can be used both as a stand-alone application and as an applet.  Note that
+the option \texttt{-g} of \texttt{isatool usedir} (see
+\S\ref{sec:tool-usedir}) creates graph presentations in batch mode for
+inclusion in session documents.
 
 
 \subsection{Invoking the graph browser}
@@ -145,12 +162,12 @@
 \subsection{Using the graph browser}
 
 The browser's main window, which is shown in figure
-\ref{browserwindow}, consists of two sub-windows: In the left
+\ref{fig:browserwindow}, consists of two sub-windows: In the left
 sub-window, the directory tree is displayed. The graph itself is
 displayed in the right sub-window.
 \begin{figure}[ht]
   \includegraphics[width=\textwidth]{browser_screenshot}
-  \caption{\label{browserwindow} Browser main window}
+  \caption{\label{fig:browserwindow} Browser main window}
 \end{figure}
 
 
@@ -205,7 +222,7 @@
 \item[Open \dots] Open a new graph file.
   
 \item[Export to PostScript] Outputs the current graph in Postscript format,
-  appropriately scaled to fit on one single sheet of paper.  The resulting
+  appropriately scaled to fit on one single sheet of A4 paper.  The resulting
   file can be printed directly.
   
 \item[Export to EPS] Outputs the current graph in Encapsulated Postscript
@@ -250,115 +267,6 @@
 \end{description}
 
 
-\section{Preparing Isabelle session documents --- \texttt{isatool document}}
-\label{sec:tool-document}
-
-The \tooldx{document} utility prepares logic session documents, processing the
-sources both as provided by the user and generated by Isabelle.  Its usage is:
-\begin{ttbox}
-Usage: document [OPTIONS] [DIR]
-
-  Options are:
-    -c           cleanup -- be aggressive in removing old stuff
-    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf
-    -v           be verbose
-
-  Prepare the theory session document in DIR (default 'document')
-  producing the specified output format.
-\end{ttbox}
-This tool is usually run automatically as part of the corresponding session,
-provided document preparation has been enabled (cf.\ the \texttt{-d} option of
-the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).  It may be manually
-invoked on the generated browser information document output as well.
-
-\medskip Document preparation requires a properly setup ``\texttt{document}''
-directory within the logic session sources.  This directory is supposed to
-contain all the files needed to produce the final document --- apart from the
-actual theories which are generated by Isabelle.
-
-\medskip For simple documents, the \texttt{document} tool is smart enough to
-create any of the output formats, taking \texttt{root.tex} supplied by the
-user as a starting point.  This even includes multiple runs of {\LaTeX} to
-accommodate references and bibliographies (the latter assumes
-\texttt{root.bib} within the same directory).
-
-For complex documents, a separate \texttt{IsaMakefile} may be given instead.
-It should provide targets for any admissible document format; these have to
-produce corresponding output files named after \texttt{root} as well, e.g.\ 
-\texttt{root.dvi} for target format \texttt{dvi}.
-
-\medskip When running the session, Isabelle copies the original
-\texttt{document} directory into its proper place within
-\texttt{ISABELLE_BROWSER_INFO} according to the session path.  Then, for any
-processed theory $A$ some {\LaTeX} source is generated and put there as
-$A$\texttt{.tex}.  Furthermore, a list of all generated theory files is put
-into \texttt{session.tex}.  Typically, the root {\LaTeX} file provided by the
-user would include \texttt{session.tex} to get a document containing all the
-theories.
-
-The {\LaTeX} versions of the theories require some macros defined in
-\texttt{isabelle.sty} as distributed with Isabelle.  Doing
-\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
-the underlying Isabelle \texttt{latex} utility already includes an appropriate
-{\TeX} inputs path.
-
-If the text contains any references to Isabelle symbols (such as
-\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
-This package contains a standard set of {\LaTeX} macro definitions
-\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
-Appendix~\ref{app:symbols} for a complete list).  The user may refer to
-further symbols as well, simply by providing {\LaTeX} macros of the same sort.
-
-For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
-images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
-do so even without using PDF~\LaTeX.
-
-\medskip As a final step, \texttt{isatool document -c} is run on the resulting
-\texttt{document} directory.  Thus the actual output document is built and
-installed in its proper place (as linked by the session's
-\texttt{index.html}).  The generated sources are deleted after successful run
-of {\LaTeX} and friends.  Note that a copy of the sources may be retained by
-passing an option \texttt{-D} to the \texttt{usedir} utility when running the
-session (see also \S\ref{sec:tool-usedir}).
-
-
-\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
-\label{sec:tool-latex}
-
-The \tooldx{latex} utility provides the basic interface for Isabelle document
-preparation.  Its usage is:
-\begin{ttbox}
-Usage: latex [OPTIONS] [FILE]
-
-  Options are:
-    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
-                 ps.gz, pdf, bbl, png, sty
-
-  Run LaTeX (and related tools) on FILE (default root.tex),
-  producing the specified output format.
-\end{ttbox}
-Appropriate {\LaTeX}-related programs are run on the input file, according to
-the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
-\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
-The actual commands are determined from the settings environment
-(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
-
-The \texttt{sty} 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 (cf.\ 
-option \texttt{-D} of the \texttt{usedir} utility, see
-\S\ref{sec:tool-usedir}).
-
-It is important to note that the {\LaTeX} inputs file space has to be properly
-setup to include the Isabelle styles.  Usually, this may be done by modifying
-the \settdx{TEXINPUTS} variable in settings like this:
-\begin{ttbox}
-TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
-\end{ttbox}
-This is known to work with recent versions of the \textsl{teTeX} distribution.
-
-
 \section{Creating Isabelle session directories --- \texttt{isatool mkdir}}
 \label{sec:tool-mkdir}
 
@@ -367,7 +275,7 @@
 and a \texttt{document} directory with a minimal \texttt{root.tex} that is
 sufficient print all theories of the session (in the order of appearance); see
 \S\ref{sec:tool-document} for further information on Isabelle document
-preparation.  The usage of \texttt{mkdir} is:
+preparation.  The usage of \texttt{isatool mkdir} is:
 \begin{ttbox}
 Usage: mkdir [OPTIONS] [LOGIC] NAME
 
@@ -383,7 +291,7 @@
 
 The \texttt{mkdir} tool is conservative in the sense that any existing
 \texttt{IsaMakefile} etc.\ is left unchanged.  Thus it is safe to invoke it
-experimentally, with varying options.
+multiple times, although later runs may not have the desired effect.
 
 Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}
 incrementally --- manual changes are required for multiple sub-sessions.  On
@@ -420,16 +328,23 @@
 The standard setup of a single ``example session'' based on the default logic,
 with proper document generation is generated like this:
 \begin{ttbox}
-isatool mkdir Foo
-isatool make
+isatool mkdir Foo && isatool make
 \end{ttbox}
 \noindent The theory sources should be put into the \texttt{Foo} directory, and its
 \texttt{ROOT.ML} should be edited to load all required theories.  Invoking
-\texttt{isatool make} would now run the whole session, generating browser
+\texttt{isatool make} again would run the whole session, generating browser
 information and the document automatically.  The \texttt{IsaMakefile} is
-usually tuned manually later, e.g.\ adding actual source dependencies, or
+typically tuned manually later, e.g.\ adding actual source dependencies, or
 changing the options passed to \texttt{usedir}.
 
+\medskip Large projects may demand further sessions, potentially with separate
+logic images being created.  This usually requires manual editing of the
+generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session
+directories at the same time (this is the deeper reasong why
+\texttt{IsaMakefile} is not made part of the initial session directory created
+by \texttt{isatool mkdir}).  See \texttt{src/HOL/IsaMakefile} of the Isabelle
+distribution for a full-blown example.
+
 
 \section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
 
@@ -445,6 +360,7 @@
     -b           build mode (output heap image, using current dir)
     -c BOOL      tell ML system to compress output image (default true)
     -d FORMAT    build document as FORMAT (default false)
+    -g BOOL      generate session graph image for document (default false)
     -i BOOL      generate theory browser information (default false)
     -m MODE      add print mode for output
     -p LEVEL     set level of detail for proof objects
@@ -500,6 +416,14 @@
 \texttt{document} directory.  See \S\ref{sec:tool-document} and
 \S\ref{sec:tool-latex} for more details.
 
+The \texttt{-g} option produces images of the theory dependency graph (cf.\ 
+\S\ref{sec:browse}) for inclusion in the generated document, both as
+\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
+In order to make this appear the final {\LaTeX} document one would typically
+say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
+file.  (Omitting the file-name extension enables {\LaTeX} to select to correct
+version, either for the DVI or PDF output path.)
+
 \medskip The \texttt{-D} option causes the generated document sources to be
 dumped at location \texttt{PATH}, which is relative to the session's main
 directory.  For example, \texttt{-D document} would leave a copy of the
@@ -533,6 +457,135 @@
 \S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
 of \texttt{usedir} as well.
 
+
+\section{Preparing Isabelle session documents --- \texttt{isatool document}}
+\label{sec:tool-document}
+
+The \tooldx{document} utility prepares logic session documents, processing the
+sources both as provided by the user and generated by Isabelle.  Its usage is:
+\begin{ttbox}
+Usage: document [OPTIONS] [DIR]
+
+  Options are:
+    -c           cleanup -- be aggressive in removing old stuff
+    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
+                 ps.gz, pdf
+
+  Prepare the theory session document in DIR (default 'document')
+  producing the specified output format.
+\end{ttbox}
+This tool is usually run automatically as part of the corresponding Isabelle
+batch process, provided document preparation has been enabled (cf.\ the
+\texttt{-d} option of the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).
+It may be manually invoked on the generated browser information document
+output as well, e.g.\ in case of errors encountered in the batch run.
+
+\medskip Document preparation requires a properly setup ``\texttt{document}''
+directory within the logic session sources.  This directory is supposed to
+contain all the files needed to produce the final document --- apart from the
+actual theories which are generated by Isabelle.
+
+\medskip For most practical purposes, the \texttt{document} tool is smart
+enough to create any of the specified output formats, taking \texttt{root.tex}
+supplied by the user as a starting point.  This even includes multiple runs of
+{\LaTeX} to accommodate references and bibliographies (the latter assumes
+\texttt{root.bib} within the same directory).
+
+In more complex situations, a separate \texttt{IsaMakefile} for the document
+sources may be given instead.  This should provide targets for any admissible
+document format; these have to produce corresponding output files named after
+\texttt{root} as well, e.g.\ \texttt{root.dvi} for target format \texttt{dvi}.
+
+\medskip When running the session, Isabelle copies the original
+\texttt{document} directory into its proper place within
+\texttt{ISABELLE_BROWSER_INFO} according to the session path.  Then, for any
+processed theory $A$ some {\LaTeX} source is generated and put there as
+$A$\texttt{.tex}.  Furthermore, a list of all generated theory files is put
+into \texttt{session.tex}.  Typically, the root {\LaTeX} file provided by the
+user would include \texttt{session.tex} to get a document containing all the
+theories.
+
+The {\LaTeX} versions of the theories require some macros defined in
+\texttt{isabelle.sty} as distributed with Isabelle.  Doing
+\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
+the underlying Isabelle \texttt{latex} utility already includes an appropriate
+{\TeX} inputs path.
+
+If the text contains any references to Isabelle symbols (such as
+\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
+This package contains a standard set of {\LaTeX} macro definitions
+\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
+Appendix~\ref{app:symbols} 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 \texttt{isabellesym.sty} of the
+distribution.
+
+For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
+images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
+do so even without using PDF~\LaTeX.
+
+\medskip As a final step of document preparation within Isabelle,
+\texttt{isatool document -c} is run on the resulting \texttt{document}
+directory.  Thus the actual output document is built and installed in its
+proper place (as linked by the session's \texttt{index.html} if option
+\texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{sec:info}).  The
+generated sources are deleted after successful run of {\LaTeX} and friends.
+Note that a separate copy of the sources may be retained by passing an option
+\texttt{-D} to the \texttt{usedir} utility when running the session (see also
+\S\ref{sec:tool-usedir}).
+
+
+\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
+\label{sec:tool-latex}
+
+The \tooldx{latex} utility provides the basic interface for Isabelle document
+preparation.  Its usage is:
+\begin{ttbox}
+Usage: latex [OPTIONS] [FILE]
+
+  Options are:
+    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
+                 ps.gz, pdf, bbl, png, sty
+
+  Run LaTeX (and related tools) on FILE (default root.tex),
+  producing the specified output format.
+\end{ttbox}
+Appropriate {\LaTeX}-related programs are run on the input file, according to
+the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
+\texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
+The actual commands are determined from the settings environment
+(\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
+
+The \texttt{sty} 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 (cf.\ 
+option \texttt{-D} of the \texttt{usedir} utility, see
+\S\ref{sec:tool-usedir}).
+
+It is important to note that the {\LaTeX} inputs file space has to be properly
+setup to include the Isabelle styles.  Usually, this may be done by modifying
+the \settdx{TEXINPUTS} variable in the Isabelle settings like this:
+\begin{ttbox}
+TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
+\end{ttbox}
+This is known to work with \textsl{teTeX} (version 1.0 or later).
+
+
+\subsubsection*{Examples}
+
+Invoking \texttt{isatool latex} by hand may be occasionally useful when
+debugging failed attempts of the automatic document preparation stage of
+batch-mode Isabelle.  The abortive process leaves the sources at a certain
+place within \texttt{ISABELLE_BROWSER_INFO}, see the runtime error message for
+details.  This enables users to inspect {\LaTeX} runs in further detail, e.g.\ 
+like this:
+
+\begin{ttbox}
+  cd ~/isabelle/browser_info/HOL/Test/document
+  isatool latex -o pdf
+\end{ttbox}
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "system"




