# HG changeset patch
# User wenzelm
# Date 880123022 -3600
# Node ID 2048e7a79d09d215e512fb5fb6caa00e02d57994
# Parent  c9b577c8f7a1bf1cb7d00f79a173448003aee4ee
cd, use: path variables;

diff -r c9b577c8f7a1 -r 2048e7a79d09 doc-src/Ref/introduction.tex
--- 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}