doc-src/System/basics.tex

 usage is:
 \begin{ttbox}
 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
+    -I           startup Isar interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -m MODE      add print mode for output
     -q           non-interactive session
     -r           open heap file read-only
     -u           pass 'use"ROOT.ML";' to the ML session

 \medskip The \texttt{-m} option adds identifiers of print modes to be
 made active for this session. Typically, this is used by some user
 interface, for example to enable output of mathematical symbols from a
 special screen font.
 
-\medskip Isabelle normally enters an interactice {\ML} top-level loop
-(after processing the \texttt{-e} texts). The \texttt{-q} option
-inhibits this, thus providing a pure batch mode facility.
+\medskip Isabelle normally enters an interactice top-level loop (after
+processing the \texttt{-e} texts). The \texttt{-q} option inhibits this, thus
+providing a pure batch mode facility.
+
+\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
+startup, instead of the primitive {\ML} top-level.  This flag is usually
+enabled by default when running Isabelle via some user interface, but it is
+\emph{not} for the basic \texttt{isabelle} program.
 
 
 \subsection*{Examples}
 
 Run an interactive session of the default object-logic (as specified