# HG changeset patch
# User wenzelm
# Date 1165522125 -3600
# Node ID a9fdad55a53d832fef41bb97ca373fd651d66938
# Parent  9300bec44e6a8c726c4e2966684aff62db9f3d3f
removed obsolete references to ProofGeneral/isa;

diff -r 9300bec44e6a -r a9fdad55a53d doc-src/IsarRef/intro.tex
--- 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.\