diff -r 35de2117b5dd -r d3ed595dd772 doc-src/System/basics.tex
--- 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: