--- a/doc-src/System/basics.tex Thu Oct 14 01:07:24 1999 +0200
+++ b/doc-src/System/basics.tex Thu Oct 14 12:46:30 1999 +0200
@@ -396,8 +396,8 @@
enabled (see \S\ref{sec:tool-installfonts} for font configuration issues).
Furthermore, different kinds of identifiers in logical terms are highlighted
appropriately, e.g.\ free variables in bold and bound variables underlined.
-There are some more options available. Just pass \texttt{-?} to the
-\texttt{xterm} interface to have its usage printed.
+There are some more options available, just pass ``\texttt{-?}'' to get the
+usage printed.
\medskip Proof~General\index{user interface!Proof General} is a much more
advanced interface. It supports both classic Isabelle (as