diff -r 13530d774a21 -r e6e1b670520b doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Sat Apr 28 17:54:50 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy	Sat Apr 28 18:05:19 2012 +0200
@@ -51,6 +51,22 @@
 *}
 
 
+section {* Shell commands within the settings environment \label{sec:tool-env} *}
+
+text {* The @{tool_def env} utility is a direct wrapper for the
+  standard @{verbatim "/usr/bin/env"} command on POSIX systems,
+  running within the Isabelle settings environment
+  (\secref{sec:settings}).
+
+  The command-line arguments are that of the underlying version of
+  @{verbatim env}.  For example, the following invokes an instance of
+  the GNU Bash shell within the Isabelle environment:
+\begin{alltt}
+  isabelle env bash
+\end{alltt}
+*}
+
+
 section {* Getting logic images *}
 
 text {*