--- a/doc-src/IsarRef/Thy/Misc.thy Sun Oct 10 19:49:18 2010 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Sun Oct 10 20:12:10 2010 +0100
@@ -143,7 +143,7 @@
\end{matharray}
\begin{rail}
- ('cd' | 'use\_thy' | 'update\_thy') name
+ ('cd' | 'use\_thy') name
;
\end{rail}
@@ -159,6 +159,13 @@
since loading of theories is done automatically as required.
\end{description}
+
+ %FIXME proper place (!?)
+ Isabelle file specification may contain path variables (e.g.\
+ @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly. Note
+ that @{verbatim "~"} abbreviates @{verbatim "$HOME"}, and @{verbatim
+ "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The general syntax
+ for path specifications follows POSIX conventions.
*}
end
--- a/doc-src/IsarRef/Thy/document/Misc.tex Sun Oct 10 19:49:18 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Sun Oct 10 20:12:10 2010 +0100
@@ -164,7 +164,7 @@
\end{matharray}
\begin{rail}
- ('cd' | 'use\_thy' | 'update\_thy') name
+ ('cd' | 'use\_thy') name
;
\end{rail}
@@ -179,7 +179,13 @@
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
- \end{description}%
+ \end{description}
+
+ %FIXME proper place (!?)
+ Isabelle file specification may contain path variables (e.g.\
+ \verb|$ISABELLE_HOME|) that are expanded accordingly. Note
+ that \verb|~| abbreviates \verb|$HOME|, and \verb|~~| abbreviates \verb|$ISABELLE_HOME|. The general syntax
+ for path specifications follows POSIX conventions.%
\end{isamarkuptext}%
\isamarkuptrue%
%