doc-src/System/present.tex
changeset 7861 8d5d3163fd81
parent 7849 29a2a1d71128
child 7868 0cb6508f190c
--- 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]