# HG changeset patch
# User wenzelm
# Date 1363276176 -3600
# Node ID e19a22974c7297da2f163f53f6eed2b0c7c70cbb
# Parent  48eb29821bd9c988aa22fb354be310e2b82684b3
document ISABELLE_POLYML;

diff -r 48eb29821bd9 -r e19a22974c72 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Thu Mar 14 14:25:55 2013 +0100
+++ b/src/Doc/System/Basics.thy	Thu Mar 14 16:49:36 2013 +0100
@@ -221,6 +221,13 @@
   automatically obtained by composing the values of @{setting
   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
 
+  \item[@{setting_def ISABELLE_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
+  for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
+  SML/NJ where it is empty.  This is particularly useful with the
+  build option @{system_option condition}
+  (\secref{sec:system-options}) to restrict big sessions to something
+  that SML/NJ can still handle.
+
   \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
   (Java Development Kit) installation with @{verbatim javac} and
   @{verbatim jar} executables.  This is essential for Isabelle/Scala