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>\-l\ option specifies the logic session name. By default, its heap image is checked and built on demand, but the option \<^verbatim>\-n\ skips that. + Option \<^verbatim>\-r\ abbreviates \<^verbatim>\-l RAW_ML_SYSTEM\, which is relevant to bootstrap + Isabelle/Pure interactively. + Options \<^verbatim>\-d\, \<^verbatim>\-o\, \<^verbatim>\-s\ are passed directly to @{tool build} (\secref{sec:tool-build}).