# HG changeset patch
# User wenzelm
# Date 1371720463 -7200
# Node ID f00e4d8dde4c1d02560133c43a484c2e6cb6c11e
# Parent  0590d4a83035b563afba061ca9dedaf0f05bd95f
updated to Isabelle2013;

diff -r 0590d4a83035 -r f00e4d8dde4c src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Thu Jun 20 11:08:54 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Thu Jun 20 11:27:43 2013 +0200
@@ -1562,14 +1562,9 @@
   to support \emph{implicit parallelism} to a large extent.  LCF-style
   theorem provides almost ideal conditions for that, see also
   \cite{Wenzel:2009}.  This means, significant parts of theory and
-  proof checking is parallelized by default.  A maximum speedup-factor
-  of 3.0 on 4 cores and 5.0 on 8 cores can be
-  expected.\footnote{Further scalability is limited due to garbage
-  collection, which is still sequential in Poly/ML 5.2/5.3/5.4.  It
-  helps to provide initial heap space generously, using the
-  \texttt{-H} option.  Initial heap size needs to be scaled-up
-  together with the number of CPU cores: approximately 1--2\,GB per
-  core..}
+  proof checking is parallelized by default.  In Isabelle2013, a
+  maximum speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be
+  expected.
 
   \medskip ML threads lack the memory protection of separate
   processes, and operate concurrently on shared heap memory.  This has
@@ -1753,9 +1748,8 @@
   continue.  The @{text "name"} argument is used for tracing and might
   help to spot sources of congestion.
 
-  Entering the critical section without contention is very fast, and
-  several basic system operations do so frequently.  Each thread
-  should stay within the critical section quickly only very briefly,
+  Entering the critical section without contention is very fast.  Each
+  thread should stay within the critical section only very briefly,
   otherwise parallel performance may degrade.
 
   \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty