# HG changeset patch
# User wenzelm
# Date 1345023687 -7200
# Node ID b0c39fd53c0e800f2d4e1c98d24bc3476c19d678
# Parent  9509fc5485b2538a4f8557ce173fc69be33bf79a
tuned;

diff -r 9509fc5485b2 -r b0c39fd53c0e doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Wed Aug 15 11:04:56 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy	Wed Aug 15 11:41:27 2012 +0200
@@ -27,7 +27,7 @@
   of the actual ML system to be used.  Regular users rarely need to
   care about the low-level process.
 
-  \item The main \emph{Isabelle tools wrapper} (@{executable_ref
+  \item The main \emph{Isabelle tool wrapper} (@{executable_ref
   isabelle}) provides a generic startup environment Isabelle related
   utilities, user interfaces etc.  Such tools automatically benefit
   from the settings mechanism.
@@ -491,7 +491,7 @@
 *}
 
 
-section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
+section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
 
 text {*
   All Isabelle related tools and interfaces are called via a common
@@ -520,9 +520,8 @@
 
 subsubsection {* Examples *}
 
-text {*
-  Show the list of available documentation of the current Isabelle
-  installation like this:
+text {* Show the list of available documentation of the Isabelle
+  distribution:
 
 \begin{ttbox}
   isabelle doc
@@ -533,14 +532,10 @@
   isabelle doc system
 \end{ttbox}
 
-  Create an Isabelle session derived from HOL (see also
-  \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+  Query the Isabelle settings environment:
 \begin{ttbox}
-  isabelle mkdir HOL Test && isabelle make
+  isabelle getenv ISABELLE_HOME_USER
 \end{ttbox}
-  Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
-  existing sessions (including document output etc.) are then updated
-  by @{verbatim "isabelle make"} alone.
 *}
 
 end
\ No newline at end of file
diff -r 9509fc5485b2 -r b0c39fd53c0e doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Wed Aug 15 11:04:56 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Wed Aug 15 11:41:27 2012 +0200
@@ -45,7 +45,7 @@
   of the actual ML system to be used.  Regular users rarely need to
   care about the low-level process.
 
-  \item The main \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}) provides a generic startup environment Isabelle related
+  \item The main \emph{Isabelle tool wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}) provides a generic startup environment Isabelle related
   utilities, user interfaces etc.  Such tools automatically benefit
   from the settings mechanism.
 
@@ -505,7 +505,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
+\isamarkupsection{The Isabelle tool wrapper \label{sec:isabelle-tool}%
 }
 \isamarkuptrue%
 %
@@ -538,8 +538,8 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Show the list of available documentation of the current Isabelle
-  installation like this:
+Show the list of available documentation of the Isabelle
+  distribution:
 
 \begin{ttbox}
   isabelle doc
@@ -550,14 +550,10 @@
   isabelle doc system
 \end{ttbox}
 
-  Create an Isabelle session derived from HOL (see also
-  \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+  Query the Isabelle settings environment:
 \begin{ttbox}
-  isabelle mkdir HOL Test && isabelle make
-\end{ttbox}
-  Note that \verb|isabelle mkdir| is usually only invoked once;
-  existing sessions (including document output etc.) are then updated
-  by \verb|isabelle make| alone.%
+  isabelle getenv ISABELLE_HOME_USER
+\end{ttbox}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %