--- a/doc-src/IsarRef/intro.tex Thu Dec 07 17:58:54 2006 +0100
+++ b/doc-src/IsarRef/intro.tex Thu Dec 07 21:08:45 2006 +0100
@@ -88,14 +88,14 @@
\subsubsection{Proof~General as default Isabelle interface}
The Isabelle interface wrapper script provides an easy way to invoke
-Proof~General (including XEmacs or GNU Emacs). The default configuration of
-Isabelle is smart enough to detect the Proof~General distribution in several
-canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus
-the capital \texttt{Isabelle} executable would already refer to the
-\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
- also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
- ML.} The Isabelle interface script provides several options; pass \verb,-?,
-to see its usage.
+Proof~General (including XEmacs or GNU Emacs). The default
+configuration of Isabelle is smart enough to detect the Proof~General
+distribution in several canonical places (e.g.\
+\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
+\texttt{Isabelle} executable would already refer to the
+\texttt{ProofGeneral/isar} interface without further ado. The
+Isabelle interface script provides several options; pass \verb,-?, to
+see its usage.
With the proper Isabelle interface setup, Isar documents may now be edited by
visiting appropriate theory files, e.g.\