--- a/doc-src/System/basics.tex Wed Aug 18 15:40:45 1999 +0200
+++ b/doc-src/System/basics.tex Wed Aug 18 16:04:00 1999 +0200
@@ -391,18 +391,18 @@
\medskip
-ProofGeneral\index{user interface!ProofGeneral} of LFCS Edinburgh is another,
-much more advanced interface. It supports both classic Isabelle (as
+Proof~General\index{user interface!Proof General} of LFCS Edinburgh is
+another, much more advanced interface. It supports both classic Isabelle (as
\texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}).
Note that the latter is slightly better supported, and more robust.
-ProofGeneral already ships with appropriate executable scripts to be run as
-Isabelle interface. Thus a typical setup of ProofGeneral for Isabelle/Isar
+Proof~General already ships with appropriate executable scripts to be run as
+Isabelle interface. Thus a typical setup of Proof~General for Isabelle/Isar
would be like this:
\begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
PROOFGENERAL_OPTIONS="-p emacs -u true"
\end{ttbox}
-See \cite{proofgeneral} for more information on ProofGeneral.
+See \cite{proofgeneral} for more information on Proof~General.
%%% Local Variables: