doc-src/System/Thy/document/Misc.tex

 \isamarkupsection{Output the version identifier of the Isabelle distribution%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility outputs the full version string of
-  the Isabelle distribution being used, e.g.\ ``\verb|Isabelle2008: June 2008|.  There are no options nor arguments.%
+The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility displays Isabelle version information:
+\begin{ttbox}
+Usage: isabelle version [OPTIONS]
+
+  Options are:
+    -i           short identification (derived from Mercurial id)
+
+  Display Isabelle version information.
+\end{ttbox}
+
+  \medskip The default is to output the full version string of the
+  Isabelle distribution, e.g.\ ``\verb|Isabelle2008: June 2008|.
+
+  The \verb|-i| option produces a short identification derived
+  from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Convert XML to YXML%
 }