--- 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