--- a/doc-src/System/Thy/Sessions.thy Tue Aug 14 13:40:49 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Tue Aug 14 15:42:58 2012 +0200
@@ -356,19 +356,16 @@
subsubsection {* Examples *}
-text {* The following produces an example session as separate
- directory called @{verbatim Test}:
+text {* Produce session @{verbatim Test} within a separate directory
+ of the same name:
\begin{ttbox}
-isabelle mkroot Test && isabelle build -v -D Test
+isabelle mkroot Test && isabelle build -D Test
\end{ttbox}
- Option @{verbatim "-v"} is not required, but useful to reveal the
- the location of generated documents.
-
- \medskip The subsequent example turns the current directory to a
- session directory with document and builds it:
+ \medskip Upgrade the current directory into a session ROOT with
+ document preparation, and build it:
\begin{ttbox}
-isabelle mkroot -d && isabelle build -D.
+isabelle mkroot -d && isabelle build -D .
\end{ttbox}
*}