# HG changeset patch
# User wenzelm
# Date 1010594214 -3600
# Node ID ba7d930e9b0dc0c174608814017c8967afaf5efa
# Parent  4ad13c2f7196381feb690cdf705d57f778234bc2
no longer requires TEXINPUTS;

diff -r 4ad13c2f7196 -r ba7d930e9b0d doc-src/System/present.tex
--- a/doc-src/System/present.tex	Wed Jan 09 17:36:34 2002 +0100
+++ b/doc-src/System/present.tex	Wed Jan 09 17:36:54 2002 +0100
@@ -438,8 +438,8 @@
 directory.  For example, \texttt{-D document} would leave a copy of the
 {\LaTeX} sources in the actual document directory.  Thus the Isabelle
 \texttt{document} or \texttt{latex} tools may be run later, facilitating much
-easier debugging of {\LaTeX} errors, for example.  Note that a copy of the
-Isabelle style files will be placed in \texttt{PATH} as well.
+easier debugging of {\LaTeX} errors, for example.  A copy of the Isabelle
+style files will be placed in \texttt{PATH} as well.
 
 \medskip The \texttt{-p} option determines the level of detail for internal
 proof objects, see also the \emph{Isabelle Reference
@@ -571,14 +571,6 @@
 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}