# HG changeset patch
# User wenzelm
# Date 1116346234 -7200
# Node ID 38db39971a5ae469ef0b9fb836f8ee4e00fe4331
# Parent  3dfcdb19f24202023daae662c38f5e303b49d930
no longer support isa-FOO interface;
removed Isamode;
tuned;

diff -r 3dfcdb19f242 -r 38db39971a5a doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Tue May 17 18:10:33 2005 +0200
+++ b/doc-src/System/basics.tex	Tue May 17 18:10:34 2005 +0200
@@ -391,50 +391,33 @@
 Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
 \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
 uniform way for end-users to invoke a certain interface; which one to start is
-determined by the \settdx{ISABELLE_INTERFACE} setting variable.  Also note
-that the \texttt{install} utility provides some options to install desktop
-environment icons as well (see \S\ref{sec:tool-install}).
-
-An interface may be specified either by giving an identifier that the Isabelle
-distribution knows about, or by specifying an actual path name (containing a
-slash ``\texttt{/}'') of some executable.  Currently, the following interfaces
-are available:
-
-\begin{itemize}
-\item \texttt{none} is just a pass-through to raw \texttt{isabelle}. Thus
-  \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.  This is
-  the factory default.
+determined by the \settdx{ISABELLE_INTERFACE} setting variable, which should
+give a full path specification to the actual executable.  Also note that the
+\texttt{install} utility provides some options to install desktop environment
+icons (see \S\ref{sec:tool-install}).
 
-\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
-  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}
+Presently, the most prominent Isabelle interface is
+Proof~General~\cite{proofgeneral}\index{user interface!Proof General}.  There
+are separate versions for the raw ML top-level and the proper Isabelle/Isar
+interpreter loop.  The Proof~General distribution includes separate interface
+wrapper scripts (in \texttt{ProofGeneral/isa} and \texttt{ProofGeneral/isar})
+for either of these.  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 by default, or
-  \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
-  to switch between the Isar and ML view, independently of the interface
-  script being used.
+\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 by default, or \texttt{-m}
+to tune the standard print mode.  The \texttt{-I} option allows to switch
+between the Isar and ML view, independently of the interface script being
+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}
+\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.
 
 %%% Local Variables:
 %%% mode: latex