diff -r 2373b4c61111 -r 577f029fde39 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Mon Jun 30 10:34:28 2014 +0200
+++ b/src/Doc/System/Misc.thy	Mon Jun 30 10:53:37 2014 +0200
@@ -309,41 +309,6 @@
 *}
 
 
-section {* Proof General / Emacs *}
-
-text {* The @{tool_def emacs} tool invokes a version of Emacs and
-  Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
-  regular Isabelle settings environment (\secref{sec:settings}).  This
-  is more convenient than starting Emacs separately, loading the Proof
-  General LISP files, and then attempting to start Isabelle with
-  dynamic @{setting PATH} lookup etc., although it might fail if a
-  different version of Proof General is already part of the Emacs
-  installation of the operating system.
-
-  The actual interface script is part of the Proof General
-  distribution; 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 of the prover process.  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.  This is
-  implicitly provided for versions of Proof General that are
-  distributed as Isabelle component, see also \secref{sec:components};
-  otherwise it needs to be configured manually.
-
-  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
-  the command line of any invocation of the Proof General @{verbatim
-  interface} script.  This allows to provide persistent default
-  options for the invocation of \texttt{isabelle emacs}.
-
-  \end{description}
-*}
-
-
 section {* Shell commands within the settings environment \label{sec:tool-env} *}
 
 text {* The @{tool_def env} tool is a direct wrapper for the standard