# HG changeset patch
# User wenzelm
# Date 1427921209 -7200
# Node ID 9d04e2c188b3af0da229de7c65baa52e1b421e55
# Parent  9d70a39d1cf30287864cf198cd4470aaf06cb455
tuned;

diff -r 9d70a39d1cf3 -r 9d04e2c188b3 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Apr 01 22:40:41 2015 +0200
+++ b/src/Doc/System/Basics.thy	Wed Apr 01 22:46:49 2015 +0200
@@ -402,9 +402,9 @@
 
   The read-write state of sessions is determined at startup only, it
   cannot be changed intermediately. Also note that heap images may
-  require considerable amounts of disk space (approximately
-  50--200~MB). Users are responsible for themselves to dispose their
-  heap files when they are no longer needed.
+  require considerable amounts of disk space (hundreds of MB or some GB).
+  Users are responsible for themselves to dispose their heap files
+  when they are no longer needed.
 
   \medskip The @{verbatim "-w"} option makes the output heap file
   read-only after terminating.  Thus subsequent invocations cause the