# HG changeset patch
# User wenzelm
# Date 939897990 -7200
# Node ID 8d5d3163fd814c5f69d0a906d61a0c28674a6b9e
# Parent  7819547df4d81c91935308d01ef965584f6a8788
tuned;

diff -r 7819547df4d8 -r 8d5d3163fd81 doc-src/System/basics.tex
--- 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
diff -r 7819547df4d8 -r 8d5d3163fd81 doc-src/System/present.tex
--- 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]