removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
separate chapter on interfaces as Isabelle tools;

--- a/doc-src/System/IsaMakefile	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/IsaMakefile	Sun Nov 30 14:03:46 2008 +0100
@@ -22,7 +22,7 @@
 Pure-System: $(LOG)/Pure-System.gz
 
 $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
-  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
+  Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
 	@$(USEDIR) -s System Pure Thy
 
 

--- a/doc-src/System/Thy/Basics.thy	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/Thy/Basics.thy	Sun Nov 30 14:03:46 2008 +0100
@@ -8,19 +8,18 @@
 
 text {*
   This manual describes Isabelle together with related tools and user
-  interfaces as seen from an outside (system oriented) view.  See also
-  the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
-  and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
-  actual Isabelle commands and related functions.
+  interfaces as seen from a system oriented view.  See also the
+  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
+  the actual Isabelle input language and related concepts.
 
-  \medskip The Isabelle system environment emerges from a few general
-  concepts.
+  \medskip The Isabelle system environment provides the following
+  basic infrastructure to integrate tools smoothly.
 
   \begin{enumerate}
 
-  \item The \emph{Isabelle settings} mechanism provides environment
-  variables to all Isabelle programs (including tools and user
-  interfaces).
+  \item The \emph{Isabelle settings} mechanism provides process
+  environment variables to all Isabelle executables (including tools
+  and user interfaces).
 
   \item The \emph{raw Isabelle process} (@{executable_ref
   "isabelle-process"}) runs logic sessions either interactively or in
@@ -33,11 +32,6 @@
   user interfaces etc.  Such tools automatically benefit from the
   settings mechanism.
 
-  \item The \emph{Isabelle interface wrapper} (@{executable_ref
-  "isabelle-interface"}) provides some abstraction over the actual
-  user interface to be used.  The de-facto standard interface for
-  Isabelle is Proof~General \cite{proofgeneral}.
-
   \end{enumerate}
 *}
 
@@ -256,11 +250,6 @@
   derives an individual directory for temporary files.  The default is
   somewhere in @{verbatim "/tmp"}.
   
-  \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
-  specifies the actual user interface that the capital @{executable
-  Isabelle} or @{executable "isabelle-interface"} should invoke.  See
-  \secref{sec:interface} for more details.
-
   \end{description}
 *}
 
@@ -480,41 +469,4 @@
   by @{verbatim "isabelle make"} alone.
 *}
 
-
-section {* The Isabelle interface wrapper \label{sec:interface} *}
-
-text {*
-  Isabelle is a generic theorem prover, even w.r.t.\ its user
-  interface.  The @{executable_def Isabelle} (or @{executable_def
-  "isabelle-interface"}) executable provides a uniform way for
-  end-users to invoke a certain interface; which one to start is
-  determined by the @{setting_ref ISABELLE_INTERFACE} setting
-  variable, which should give a full path specification to the actual
-  executable.
-
-  Presently, the most prominent Isabelle interface is Proof
-  General~\cite{proofgeneral}\index{user interface!Proof General}.
-  The Proof General distribution includes an interface wrapper script
-  for the regular Isar toplevel, see @{verbatim
-  "ProofGeneral/isar/interface"}.  The canonical settings for
-  Isabelle/Isar are as follows:
-
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-
-  Thus @{executable Isabelle} would automatically invoke Emacs with
-  proper setup of the Proof General Lisp packages.  There are some
-  options available, such as @{verbatim "-l"} for passing the logic
-  image to be used by default, or @{verbatim "-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 @{executable "isabelle-process"} run from within.  This
-  requires further Emacs Lisp configuration, see the Proof General
-  documentation \cite{proofgeneral} for more information.
-*}
-
 end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/Interfaces.thy	Sun Nov 30 14:03:46 2008 +0100
@@ -0,0 +1,77 @@
+(* $Id$ *)
+
+theory Interfaces
+imports Pure
+begin
+
+chapter {* User interfaces *}
+
+section {* Plain TTY interaction \label{sec:tool-tty} *}
+
+text {*
+  The @{tool_def tty} tool runs the Isabelle process interactively
+  within a plain terminal session:
+\begin{ttbox}
+Usage: tty [OPTIONS]
+
+  Options are:
+    -l NAME      logic image name (default ISABELLE_LOGIC)
+    -m MODE      add print mode for output
+    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
+
+  Run Isabelle process with plain tty interaction, and optional line editor.
+\end{ttbox}
+
+  The @{verbatim "-l"} option specifies the logic image.  The
+  @{verbatim "-m"} option specifies additional print modes.  The The
+  @{verbatim "-p"} option specifies an alternative line editor (such
+  as the @{executable_def rlwrap} wrapper for GNU readline); the
+  fall-back is to use raw standard input.
+
+  Regular interaction is via the standard Isabelle/Isar toplevel loop.
+  The Isar command @{command exit} drops out into the raw ML system,
+  which is occasionally useful for low-level debugging.  Invoking @{ML
+  Isar.loop}~@{verbatim "();"} in ML will return to the Isar toplevel.
+*}
+
+
+section {* Proof General / Emacs *}
+
+text {*
+  The @{tool_def emacs} tool invokes a version of Emacs and Proof
+  General within the regular Isabelle settings environment
+  (\secref{sec:settings}).  This is more robust than starting Emacs
+  separately, loading the Proof General lisp files, and then
+  attempting to start Isabelle with dynamic @{setting PATH} lookup
+  etc.
+
+  The actual interface script is part of the Proof General
+  distribution~\cite{proofgeneral}; its usage depends on the
+  particular version.  There are some options available, such as
+  @{verbatim "-l"} for passing the logic image to be used by default,
+  or @{verbatim "-m"} to tune the standard print mode.  The following
+  Isabelle settings are particularly important for Proof General:
+
+  \begin{description}
+
+  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
+  installation directory of the Proof General distribution.  The
+  default settings try to locate this in a number of standard places,
+  notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
+
+  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
+  the command line of any invocation of the Proof General @{verbatim
+  interface} script.
+
+  \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
+  script to install the X11 fonts required for the X-Symbols mode of
+  Proof General.  This is only relevant if the X11 display server runs
+  on a different machine than the Emacs application, with a different
+  file-system view on the Proof General installation.  Under most
+  circumstances Proof General is able to refer to the font files that
+  are part of its distribution.
+
+  \end{description}
+*}
+
+end
\ No newline at end of file

--- a/doc-src/System/Thy/Misc.thy	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/Thy/Misc.thy	Sun Nov 30 14:03:46 2008 +0100
@@ -12,46 +12,6 @@
 *}
 
 
-section {* The Proof General / Emacs interface *}
-
-text {*
-  The @{tool_def emacs} tool invokes a version of Emacs and Proof
-  General within the regular Isabelle settings environment
-  (\secref{sec:settings}).  This is more robust than starting Emacs
-  separately, loading the Proof General lisp files, and then
-  attempting to start Isabelle with dynamic @{setting PATH} lookup
-  etc.
-
-  The actual interface script is part of the Proof General
-  distribution~\cite{proofgeneral}; its usage depends on the
-  particular version.  There are some options available, such as
-  @{verbatim "-l"} for passing the logic image to be used by default,
-  or @{verbatim "-m"} to tune the standard print mode.  The following
-  Isabelle settings are particularly important for Proof General:
-
-  \begin{description}
-
-  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
-  installation directory of the Proof General distribution.  The
-  default settings try to locate this in a number of standard places,
-  notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}.
-
-  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
-  the command line of any invocation of the Proof General @{verbatim
-  interface} script.
-
-  \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
-  script to install the X11 fonts required for the X-Symbols mode of
-  Proof General.  This is only relevant if the X11 display server runs
-  on a different machine than the Emacs application, with a different
-  file-system view on the Proof General installation.  Under most
-  circumstances Proof General is able to refer to the font files that
-  are part of its distribution.
-
-  \end{description}
-*}
-
-
 section {* Displaying documents *}
 
 text {*
@@ -294,30 +254,6 @@
 *}
 
 
-section {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *}
-
-text {*
-  The @{tool_def tty} utility runs the Isabelle process interactively
-  within a plain terminal session:
-\begin{ttbox}
-Usage: tty [OPTIONS]
-
-  Options are:
-    -l NAME      logic image name (default ISABELLE_LOGIC)
-    -m MODE      add print mode for output
-    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
-
-  Run Isabelle process with plain tty interaction, and optional line editor.
-\end{ttbox}
-
-  The @{verbatim "-l"} option specifies the logic image.  The
-  @{verbatim "-m"} option specifies additional print modes.  The The
-  @{verbatim "-p"} option specifies an alternative line editor (such
-  as the @{executable_def rlwrap} wrapper for GNU readline); the
-  fall-back is to use raw standard input.
-*}
-
-
 section {* Remove awkward symbol names from theory sources *}
 
 text {*

--- a/doc-src/System/Thy/ROOT.ML	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/Thy/ROOT.ML	Sun Nov 30 14:03:46 2008 +0100
@@ -5,5 +5,6 @@
 use "../../antiquote_setup.ML";
 
 use_thy "Basics";
+use_thy "Interfaces";
 use_thy "Presentation";
 use_thy "Misc";

--- a/doc-src/System/Thy/document/Basics.tex	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/Thy/document/Basics.tex	Sun Nov 30 14:03:46 2008 +0100
@@ -26,19 +26,18 @@
 %
 \begin{isamarkuptext}%
 This manual describes Isabelle together with related tools and user
-  interfaces as seen from an outside (system oriented) view.  See also
-  the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
-  and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
-  actual Isabelle commands and related functions.
+  interfaces as seen from a system oriented view.  See also the
+  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
+  the actual Isabelle input language and related concepts.
 
-  \medskip The Isabelle system environment emerges from a few general
-  concepts.
+  \medskip The Isabelle system environment provides the following
+  basic infrastructure to integrate tools smoothly.
 
   \begin{enumerate}
 
-  \item The \emph{Isabelle settings} mechanism provides environment
-  variables to all Isabelle programs (including tools and user
-  interfaces).
+  \item The \emph{Isabelle settings} mechanism provides process
+  environment variables to all Isabelle executables (including tools
+  and user interfaces).
 
   \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either interactively or in
   batch mode.  In particular, this view abstracts over the invocation
@@ -50,10 +49,6 @@
   user interfaces etc.  Such tools automatically benefit from the
   settings mechanism.
 
-  \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) provides some abstraction over the actual
-  user interface to be used.  The de-facto standard interface for
-  Isabelle is Proof~General \cite{proofgeneral}.
-
   \end{enumerate}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -262,10 +257,6 @@
   derives an individual directory for temporary files.  The default is
   somewhere in \verb|/tmp|.
   
-  \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that
-  specifies the actual user interface that the capital \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}} should invoke.  See
-  \secref{sec:interface} for more details.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -492,43 +483,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{The Isabelle interface wrapper \label{sec:interface}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle is a generic theorem prover, even w.r.t.\ its user
-  interface.  The \indexdef{}{executable}{Isabelle}\hypertarget{executable.Isabelle}{\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}} (or \indexdef{}{executable}{isabelle-interface}\hypertarget{executable.isabelle-interface}{\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}}) executable provides a uniform way for
-  end-users to invoke a certain interface; which one to start is
-  determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting
-  variable, which should give a full path specification to the actual
-  executable.
-
-  Presently, the most prominent Isabelle interface is Proof
-  General~\cite{proofgeneral}\index{user interface!Proof General}.
-  The Proof General distribution includes an interface wrapper script
-  for the regular Isar toplevel, see \verb|ProofGeneral/isar/interface|.  The canonical settings for
-  Isabelle/Isar are as follows:
-
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-
-  Thus \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with
-  proper setup of the Proof General Lisp packages.  There are some
-  options available, such as \verb|-l| for passing the logic
-  image to be used by default, or \verb|-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 \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} run from within.  This
-  requires further Emacs Lisp configuration, see the Proof General
-  documentation \cite{proofgeneral} for more information.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isadelimtheory
 %
 \endisadelimtheory

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/document/Interfaces.tex	Sun Nov 30 14:03:46 2008 +0100
@@ -0,0 +1,115 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Interfaces}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Interfaces\isanewline
+\isakeyword{imports}\ Pure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{User interfaces%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
+  within a plain terminal session:
+\begin{ttbox}
+Usage: tty [OPTIONS]
+
+  Options are:
+    -l NAME      logic image name (default ISABELLE_LOGIC)
+    -m MODE      add print mode for output
+    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
+
+  Run Isabelle process with plain tty interaction, and optional line editor.
+\end{ttbox}
+
+  The \verb|-l| option specifies the logic image.  The
+  \verb|-m| option specifies additional print modes.  The The
+  \verb|-p| option specifies an alternative line editor (such
+  as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
+  fall-back is to use raw standard input.
+
+  Regular interaction is via the standard Isabelle/Isar toplevel loop.
+  The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
+  which is occasionally useful for low-level debugging.  Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof General / Emacs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
+  General within the regular Isabelle settings environment
+  (\secref{sec:settings}).  This is more robust than starting Emacs
+  separately, loading the Proof General lisp files, and then
+  attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
+  etc.
+
+  The actual interface script is part of the Proof General
+  distribution~\cite{proofgeneral}; its usage depends on the
+  particular version.  There are some options available, such as
+  \verb|-l| for passing the logic image to be used by default,
+  or \verb|-m| to tune the standard print mode.  The following
+  Isabelle settings are particularly important for Proof General:
+
+  \begin{description}
+
+  \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
+  installation directory of the Proof General distribution.  The
+  default settings try to locate this in a number of standard places,
+  notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
+
+  \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
+  the command line of any invocation of the Proof General \verb|interface| script.
+
+  \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
+  script to install the X11 fonts required for the X-Symbols mode of
+  Proof General.  This is only relevant if the X11 display server runs
+  on a different machine than the Emacs application, with a different
+  file-system view on the Proof General installation.  Under most
+  circumstances Proof General is able to refer to the font files that
+  are part of its distribution.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:

--- a/doc-src/System/Thy/document/Misc.tex	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/Thy/document/Misc.tex	Sun Nov 30 14:03:46 2008 +0100
@@ -30,47 +30,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{The Proof General / Emacs interface%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
-  General within the regular Isabelle settings environment
-  (\secref{sec:settings}).  This is more robust than starting Emacs
-  separately, loading the Proof General lisp files, and then
-  attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
-  etc.
-
-  The actual interface script is part of the Proof General
-  distribution~\cite{proofgeneral}; its usage depends on the
-  particular version.  There are some options available, such as
-  \verb|-l| for passing the logic image to be used by default,
-  or \verb|-m| to tune the standard print mode.  The following
-  Isabelle settings are particularly important for Proof General:
-
-  \begin{description}
-
-  \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
-  installation directory of the Proof General distribution.  The
-  default settings try to locate this in a number of standard places,
-  notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
-
-  \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
-  the command line of any invocation of the Proof General \verb|interface| script.
-
-  \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
-  script to install the X11 fonts required for the X-Symbols mode of
-  Proof General.  This is only relevant if the X11 display server runs
-  on a different machine than the Emacs application, with a different
-  file-system view on the Proof General installation.  Under most
-  circumstances Proof General is able to refer to the font files that
-  are part of its distribution.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Displaying documents%
 }
 \isamarkuptrue%
@@ -329,32 +288,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility runs the Isabelle process interactively
-  within a plain terminal session:
-\begin{ttbox}
-Usage: tty [OPTIONS]
-
-  Options are:
-    -l NAME      logic image name (default ISABELLE_LOGIC)
-    -m MODE      add print mode for output
-    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
-
-  Run Isabelle process with plain tty interaction, and optional line editor.
-\end{ttbox}
-
-  The \verb|-l| option specifies the logic image.  The
-  \verb|-m| option specifies additional print modes.  The The
-  \verb|-p| option specifies an alternative line editor (such
-  as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
-  fall-back is to use raw standard input.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Remove awkward symbol names from theory sources%
 }
 \isamarkuptrue%

--- a/doc-src/System/system.tex	Sun Nov 30 14:03:45 2008 +0100
+++ b/doc-src/System/system.tex	Sun Nov 30 14:03:46 2008 +0100
@@ -20,7 +20,7 @@
 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
 
 \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\
-  TU München}
+  TU M\"unchen}
 
 \makeindex
 
@@ -31,6 +31,7 @@
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 \input{Thy/document/Basics.tex}
+\input{Thy/document/Interfaces.tex}
 \input{Thy/document/Presentation.tex}
 \input{Thy/document/Misc.tex}