diff -r ad69aa13ddf6 -r 8b4acb408301 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Aug 16 14:22:20 1999 +0200
+++ b/doc-src/System/basics.tex	Mon Aug 16 14:22:45 1999 +0200
@@ -357,21 +357,25 @@
 
 \section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
 
-Isabelle is a generic theorem prover, even w.r.t.\ its user interface.
-The \ttindex{Isabelle} command (note the capital \texttt{I}) provides
-a uniform way for end-users to invoke a certain interface. Which one
-to actually start is determined by the \settdx{ISABELLE_INTERFACE}
-setting variable. Currently, the following are recognized:
+Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
+\ttindex{Isabelle} command (note the capital \texttt{I}) provides a uniform
+way for end-users to invoke a certain interface; which one to start actually
+is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
+
+Basically, there are two ways to specify an interface: either by giving an
+identifier that the Isabelle distribution knows about, or specifying an actual
+path name (containing a slash ``\texttt{/}'') of some executable.  Currently,
+the following interface identifiers are recognized:
 \begin{ttdescription}
 \item[none] is just a pass-through to \texttt{isabelle}. Thus
   \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
 
 \item[xterm] refers to a simple xterm based interface which is part of
   the Isabelle distribution.
-
-\item[emacs] refers to David Aspinall's \emph{Isamode} for emacs.
-  Isabelle just provides a wrapper for this, the actual Isamode
-  distribution is available elsewhere.
+  
+\item[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}.
 \end{ttdescription}
 
 The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}.
@@ -385,6 +389,21 @@
 There are some more options available.  Just pass \texttt{-?} to the
 \texttt{xterm} interface to have its usage printed.
 
+\medskip
+
+ProofGeneral\index{user interface!ProofGeneral} of LFCS Edinburgh is another,
+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 slightly better supported, and more robust.
+ProofGeneral already ships with appropriate executable scripts to be run as
+Isabelle interface.  Thus a typical setup of ProofGeneral for Isabelle/Isar
+would be like this:
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS="-p emacs -u true"
+\end{ttbox}
+See \cite{proofgeneral} for more information on ProofGeneral.
+
 
 %%% Local Variables:
 %%% mode: latex