--- a/doc-src/System/basics.tex Mon Nov 09 11:09:33 1998 +0100
+++ b/doc-src/System/basics.tex Mon Nov 09 11:20:07 1998 +0100
@@ -221,6 +221,7 @@
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
@@ -274,9 +275,14 @@
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}
--- a/doc-src/System/system.ind Mon Nov 09 11:09:33 1998 +0100
+++ b/doc-src/System/system.ind Mon Nov 09 11:20:07 1998 +0100
@@ -46,7 +46,7 @@
\item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 12, 17
\item {\tt IsaMakefile}, 11, 12
\item {\tt ISATOOL} setting, 3
- \item {\tt isatool}, 1, 6
+ \item {\tt isatool}, 1, 7
\indexspace