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

   Options are:
     -C BOOL      copy existing document directory to -D PATH (default true)
     -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 BOOL      check proofs in parallel (default true)
     -T LEVEL     multithreading: trace level (default 0)
     -V VERSION   declare alternative document VERSION
     -b           build mode (output heap image, using current dir)
     -c BOOL      tell ML system to compress output image (default true)
     -d FORMAT    build document as FORMAT (default false)

   Build object-logic or run examples. Also creates browsing
   information (HTML etc.) according to settings.
 
   ISABELLE_USEDIR_OPTIONS=
   HOL_USEDIR_OPTIONS=
+
+  ML_PLATFORM=x86-linux
+  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
+  ML_SYSTEM=polyml-5.2.1
+  ML_OPTIONS=-H 500
 \end{ttbox}
 
   Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
   setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   call. Since the \verb|IsaMakefile|s of all object-logics

   concerning the internal locking and scheduling in multithreaded
   operation.  This may be helpful in isolating performance
   bottle-necks, e.g.\ due to excessive wait states when locking
   critical code sections.
 
+  \medskip The \verb|-Q| option tells whether individual proofs
+  should be checked in parallel; the default is \verb|true|.
+  Note that fine-grained proof parallelism requires considerable
+  amounts of extra memory, since full proof context information is
+  maintained for each independent derivation thread, until checking is
+  completed.
+
   \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
   identifier}. These accumulate, documenting the way sessions depend
   on others. For example, consider \verb|Pure/FOL/ex|, which
   refers to the examples of FOL, which in turn is built upon Pure.