diff -r d7bb261e3a3b -r f666c1e4133d doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Thu Sep 27 12:24:40 2001 +0200
+++ b/doc-src/System/basics.tex	Thu Sep 27 12:25:09 2001 +0200
@@ -374,49 +374,48 @@
 
 \begin{itemize}
 \item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus
-  \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
-  
+  \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.  This is
+  the factory default.
+
 \item \texttt{xterm} refers to a simple \textsl{xterm} based interface which
   is part of the Isabelle distribution.
   
+  This interface runs \texttt{isabelle} within its own \textsl{xterm} window.
+  Usually, display of mathematical symbols from the Isabelle font is enabled
+  as well (see \S\ref{sec:tool-installfonts} for X11 font configuration
+  issues).  Furthermore, different kinds of identifiers in logical terms are
+  highlighted appropriately, e.g.\ free variables in bold and bound variables
+  underlined.  There are some more options available, just pass
+  ``\texttt{-?}'' to get the usage printed.
+  
 \item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
     interface!Isamode} for emacs.  Isabelle just provides a wrapper for this,
   the actual Isamode distribution is available elsewhere \cite{isamode}.
   
 \item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} is
-  distributed with separate interface wrapper scripts for Isabelle.  See below
-  for more details.
-\end{itemize}
-
-The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}.  This
-interface runs \texttt{isabelle} within its own \textsl{xterm} window.
-Usually, display of mathematical symbols from the Isabelle font is enabled as
-well (see \S\ref{sec:tool-installfonts} for X11 font configuration issues).
-Furthermore, different kinds of identifiers in logical terms are highlighted
-appropriately, e.g.\ free variables in bold and bound variables underlined.
-There are some more options available, just pass ``\texttt{-?}'' to get the
-usage printed.
+  an advanced interface for common theorem proving environments.  It has
+  become the de-facto standard for Isabelle recently, supporting both the old
+  ML top-level of classic Isabelle and the more convenient Isabelle/Isar
+  interpreter loop.  The Proof~General distributions includes separate
+  interface wrapper scripts (in \texttt{ProofGeneral/isa} and
+  \texttt{ProofGeneral/isar}).  The canonical settings for Isabelle/Isar are
+  as follows:
+  \begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+  \end{ttbox}
+  Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
+  the Proof~General Lisp packages.  There are some options available, such as
+  \texttt{-l} for passing the logic image to be used, or \texttt{-m} to tune
+  the standard print mode.
+  
+  \medskip Note that the world may be also seen the other way round: Emacs may
+  be started first (with proper setup of Proof~General mode), and
+  \texttt{isabelle} run from within.  This requires further Emacs Lisp
+  configuration, see the Proof~General documentation \cite{proofgeneral} for
+  more information.
 
-\medskip Proof~General\index{user interface!Proof General} is a much more
-advanced interface.  It supports both classic Isabelle (as
-\texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}).
-Note that the latter is inherently more robust.
-
-Using the Isabelle interface wrapper scripts as provided by Proof~General, a
-typical setup for Isabelle/Isar would be like this:
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS="-u false"
-\end{ttbox}
-Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
-the Proof~General Lisp packages.  There are some options available, such as
-\texttt{-l} for passing the logic image to be used.
-
-\medskip Note that the world may be also seen the other way round: Emacs may
-be started first (with proper setup of Proof~General mode), and
-\texttt{isabelle} run from within.  This requires further Emacs Lisp
-configuration, see the Proof~General documentation \cite{proofgeneral} for
-more information.
+\end{itemize}
 
 %%% Local Variables:
 %%% mode: latex