
diff -r d0b68218ea55 -r 13d6948e4b12 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Thu Mar 03 21:59:21 2016 +0100
+++ b/src/Doc/System/Misc.thy	Thu Mar 03 22:16:52 2016 +0100
@@ -65,10 +65,11 @@
 
   Options are:
     -d DIR       include session directory
-    -l NAME      logic session name (default ISABELLE_LOGIC)
+    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -r           logic session is RAW_ML_SYSTEM
     -s           system build mode for session image
 
   Run Isabelle process with raw ML console and line editor
@@ -77,6 +78,9 @@
   The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
   image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
 
+  Option \<^verbatim>\<open>-r\<close> abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+  Isabelle/Pure interactively.
+
   Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
   (\secref{sec:tool-build}).
 




