--- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 2009 +0200
@@ -299,8 +299,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
- @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
+ @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+ @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
\end{tabular}
\end{center}
@@ -454,6 +454,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -563,6 +564,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-t"} option produces a more detailed
+ internal timing report of the session.
+
\medskip The @{verbatim "-v"} option causes additional information
to be printed while running the session, notably the location of
prepared documents.