--- a/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 16:33:12 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 17:11:00 2011 +0100
@@ -472,6 +472,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -Q INT set threshold for sub-proof parallelization (default 100)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -582,8 +583,8 @@
\medskip The \verb|-q| option specifies the level of parallel
proof checking: \verb|0| no proofs, \verb|1| toplevel
proofs (default), \verb|2| toplevel and nested Isar proofs.
- The resulting speedup may vary, depending on the number of worker
- threads, granularity of proofs, and whether proof terms are enabled.
+ The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number
+ of forked proofs falls below the given value (default 100).
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.