--- 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 {*
--- a/doc-src/System/Thy/document/Misc.tex Sat Apr 28 17:54:50 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Sat Apr 28 18:05:19 2012 +0200
@@ -73,6 +73,25 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatt{env}}}}} utility is a direct wrapper for the
+ standard \verb|/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
+ \verb|env|. For example, the following invokes an instance of
+ the GNU Bash shell within the Isabelle environment:
+\begin{alltt}
+ isabelle env bash
+\end{alltt}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Getting logic images%
}
\isamarkuptrue%