--- 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
--- a/doc-src/System/present.tex Thu Oct 14 01:07:24 1999 +0200
+++ b/doc-src/System/present.tex Thu Oct 14 12:46:30 1999 +0200
@@ -84,17 +84,16 @@
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating
browser info like this:
\begin{ttbox}
-isatool usedir -i true HOL Foobar
+isatool usedir -i true HOL Foo
\end{ttbox}
-This assumes that directory \texttt{Foobar} contains some \texttt{ROOT.ML}
-file to load all your theories, and {\HOL} is your parent logic image.
-Ideally, theory browser information would have been generated for {\HOL}
-already.
+This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
+to load all your theories, and {\HOL} is your parent logic image. Ideally,
+theory browser information would have been generated for {\HOL} already.
Alternatively, one may specify an external link to an existing body of HTML
data by giving \texttt{usedir} a \texttt{-P} option like this:
\begin{ttbox}
-isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foobar
+isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
@@ -240,7 +239,7 @@
\label{sec:tool-document}
The \tooldx{document} utility prepares logic session documents, processing the
-combined sources as provided by the user and generated by Isabelle. Its usage is:
+sources both provided by the user and generated by Isabelle. Its usage is:
\begin{ttbox}
Usage: document [OPTIONS] [DIR]