# HG changeset patch
# User wenzelm
# Date 1286737930 -3600
# Node ID a194f39cfcb441a24fb76f9d2173ed9a35295683
# Parent  6cefd96bb71d0a51c60514fcc01e79b10e5d378e
note on Isabelle file specifications;
removed junk;

diff -r 6cefd96bb71d -r a194f39cfcb4 doc-src/IsarRef/Thy/Misc.thy
--- 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
diff -r 6cefd96bb71d -r a194f39cfcb4 doc-src/IsarRef/Thy/document/Misc.tex
--- 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%
 %