--- a/src/Doc/System/Sessions.thy Thu Sep 08 10:35:08 2016 +0200
+++ b/src/Doc/System/Sessions.thy Thu Sep 08 18:18:57 2016 +0200
@@ -192,6 +192,13 @@
manual adjustment (on the command-line or within personal settings or
preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
+ \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
+ space management. This is relevant for big sessions that may exhaust the
+ small 32-bit address space of the ML process (which is used by default).
+ When the option is enabled for some \isakeyword{theories} block, a full
+ sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
+ specified theories.
+
\<^item> @{system_option_def "condition"} specifies a comma-separated list of
process environment variables (or Isabelle settings) that are required for
the subsequent theories to be processed. Conditions are considered