# HG changeset patch
# User wenzelm
# Date 1363427423 -3600
# Node ID c22bd20b0d63f1ee99181de55ab52d61449eb67c
# Parent  d5c95b55f84941835fea7c0db721ac57dcdb48a6# Parent  e19a22974c7297da2f163f53f6eed2b0c7c70cbb
merged

diff -r d5c95b55f849 -r c22bd20b0d63 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Fri Mar 15 18:49:40 2013 +0100
+++ b/src/Doc/System/Basics.thy	Sat Mar 16 10:50:23 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