--- a/doc-src/Ref/introduction.tex Fri Nov 21 15:35:37 1997 +0100
+++ b/doc-src/Ref/introduction.tex Fri Nov 21 15:37:02 1997 +0100
@@ -122,7 +122,6 @@
use : string -> unit
time_use : string -> unit
\end{ttbox}
-Section~\ref{LoadingTheories} describes commands for loading theory files.
\begin{ttdescription}
\item[\ttindexbold{cd} "{\it dir}";]
changes the current directory to {\it dir}. This is the default directory
@@ -138,6 +137,12 @@
performs {\tt use~"$file$"} and prints the total execution time.
\end{ttdescription}
+The $dir$ and $file$ specifications of the \texttt{cd} and
+\texttt{use} commands may contain path variables that are expanded
+accordingly --- e.g.\ \texttt{\$ISABELLE_HOME}, or \texttt{\~\relax}
+(abbreviating \texttt{\$HOME}). Section~\ref{LoadingTheories}
+describes commands for loading theory files.
+
\section{Setting flags}
\begin{ttbox}