# HG changeset patch
# User wenzelm
# Date 1164221722 -3600
# Node ID 1e45e9ef327e295e0261e5a24c0a33707f87cc1c
# Parent  c7892915ed10582dd393c4d6d89d3fc023a0ebf6
ML_IDENTIFIER includes Isabelle version;

diff -r c7892915ed10 -r 1e45e9ef327e doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Wed Nov 22 19:53:24 2006 +0100
+++ b/doc-src/System/basics.tex	Wed Nov 22 19:55:22 2006 +0100
@@ -106,8 +106,9 @@
   absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
   executables, respectively.
   
-\item \settdx{ISABELLE_OUTPUT} will have the {\ML} system identifier
-  (according to \texttt{ML_IDENTIFIER}) automatically appended to its value.
+\item \settdx{ISABELLE_OUTPUT} will have the {\ML} system and Isabelle version
+  identifier (according to \texttt{ML_IDENTIFIER}) appended automatically to
+  its value.
 \end{itemize}
 
 \medskip The Isabelle settings scheme is conceptually simple, but not
@@ -150,16 +151,16 @@
   with \texttt{ML_OPTIONS} as first arguments on the command line.  The
   optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
   images, which is useful for cross-platform installations.  The value of
-  \texttt{ML_IDENTIFIER} is automatically obtained by composing the
-  \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM} values.
+  \texttt{ML_IDENTIFIER} is automatically obtained by composing the values of
+  \texttt{ML_SYSTEM}, \texttt{ML_PLATFORM} and the Isabelle version values.
   
 \item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons)
   where Isabelle logic images may reside.  When looking up heaps files, the
   value of \texttt{ML_IDENTIFIER} is appended to each component internally.
   
 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
-  be stored by default. The \texttt{ML_SYSTEM} identifier is appended here,
-  too.
+  be stored by default. The {\ML} system and Isabelle version identifier is
+  appended here, too.
   
 \item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
   information (HTML text, graph data, and printable documents) is stored (see