tuned;

--- a/doc-src/System/present.tex	Wed Aug 18 16:19:53 1999 +0200
+++ b/doc-src/System/present.tex	Wed Aug 18 17:15:51 1999 +0200
@@ -6,45 +6,40 @@
 \section{Generating theory browsing information} \label{sec:info}
 \index{theory browsing information|bold}
 
-Isabelle is able to generate theory browsing information, such as HTML
-documents that show a theory's definition, the theorems proved in its
-ML file and the relationship with its ancestors and descendants.
-
-Besides the HTML file that is generated for every theory, Isabelle
-stores links to all theories in an index file. These indexes are
-themself linked with other indexes to represent the hierarchic
-structure of Isabelle's logics.
+Isabelle is able to generate theory browsing information, including HTML
+documents that show a theory's definition, the theorems proved in its ML file
+and the relationship with its ancestors and descendants.  Besides the HTML
+file that is generated for every theory, Isabelle stores links to all theories
+in an index file. These indexes are linked with other indexes to represent the
+hierarchic structure of Isabelle's logics.
 
-In addition to the HTML files, Isabelle also generates \emph{graph}
-files that represent the theory hierarchy of a logic.  These graphs
-can be comfortably displayed by a graph browser Java applet embedded
-in the generated HTML pages. There is also a stand-alone version of
-the graph browser which allows browsing theory graphs without having
-to start a Web browser first. This version also includes features such
-as generating {\sc PostScript} files, which are not available in the
-applet version. The graph browser will be described later in this
-chapter.
+Isabelle also generates graph files that represent the theory hierarchy of a
+logic.  There is a graph browser Java applet embedded in the generated HTML
+pages, and also a stand-alone application that allows browsing theory graphs
+without having to start a WWW browser first.  The latter version also includes
+features such as generating {\sc PostScript} files, which are not available in
+the applet version.  See \S\ref{sec:browse} for further information.
 
-\medskip To generate theory browsing information for logics that are
-part of the Isabelle distribution, simply append ``\texttt{-i true}''
-to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.
-For example, to generate browsing information for {\FOL}, first add
-something like this to your Isabelle settings file:
+\medskip
+
+To generate theory browsing information for logics that are part of the
+Isabelle distribution, simply append ``\texttt{-i true}'' to the
+\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.  For example,
+in order to do this for {\FOL}, first add something like this to your Isabelle
+settings file
 \begin{ttbox}
 ISABELLE_USEDIR_OPTIONS="-i true"
 \end{ttbox}
-Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
-distribution and do \texttt{isatool make} (or even \texttt{isatool
-  make all}).
+and then change into the \texttt{src/FOL} directory of the Isabelle
+distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
+
+\medskip
 
-\medskip The directory in which to store theory browsing information
-is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
-The entry point to all logics is the {\tt index.html} file located in
-the directory denoted by \texttt{ISABELLE_BROWSER_INFO}.
-
-A complete HTML version of all distributed Isabelle object-logics and
-examples may be accessed on the WWW at:
-
+The theory browsing information is stored within the directory determined by
+the \settdx{ISABELLE_BROWSER_INFO} setting.  The \texttt{index.html} file
+located there provides an entry point to all standard Isabelle logics.  A
+complete HTML version of all object-logics and examples of the Isabelle
+distribution is available at
 \begin{center}\small
   \begin{tabular}{l}
     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
@@ -52,45 +47,36 @@
   \end{tabular}
 \end{center}
 
-Of course, this is not necessarily consistent with your local version!
+\medskip
 
-\medskip
-To present your own theories on the WWW, simply copy the whole
-\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
-When running your theories with the \texttt{usedir} utility, you can
-generate browsing information by specifying the option \texttt{-i true}
-on the command line, e.g.
-\begin{ttbox}
-isatool usedir -i true HOL my_theories
-\end{ttbox}
-
-The generated HTML files contain all theorems that were
-proved in the theories' \ML{} files with {\tt qed}, {\tt qed_goal} and
-{\tt qed_goalw}, or stored with {\tt bind_thm} and {\tt store_thm}.
-Additionally, there is a hypertext link to the whole \ML{} file.
-
-You can add section headings to the list of theorems by using
-
-\begin{ttbox}\index{*use_dir}
+The generated HTML document of any theory includes all theorems proved in the
+corresponding {\ML} file, provided these have been stored properly via
+\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or
+\ttindex{store_thm}.  Section headings may be included in the presentation via
+the {\ML} function
+\begin{ttbox}\index{*section}
 section: string -> unit
 \end{ttbox}
 
-in a theory's ML file, which converts a plain string to a HTML heading
-and inserts it before the next theorem proved or stored with one of
-the above functions.
+\medskip
 
-As some of Isabelle's logics are based on others (e.g. {\tt ZF}
-on {\tt FOL}) and because the HTML files list a theory's
-ancestors, you should not make HTML files for a logic if the HTML
-files for the base logic do not exist. Otherwise some of the hypertext
-links might point to non-existing documents. If the HTML files for the
-base logic are located in a directory other than \texttt{ISABELLE_BROWSER_INFO}
-or on a WWW server, you have to specify this directory or URL via
-the \texttt{-P} option, e.g.
+In order to present your own theories on the web, simply copy the whole
+\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating
+browser info like this:
 \begin{ttbox}
-isatool usedir -i true
-  -P http://isabelle.in.tum.de/library/ HOL my_theories
+isatool usedir -i true HOL Foobar
 \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.
+
+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
+\end{ttbox}
+
 
 \section{Browsing theory graphs} \label{sec:browse}
 \index{theory graph browser|bold} 

--- a/doc-src/System/system.tex	Wed Aug 18 16:19:53 1999 +0200
+++ b/doc-src/System/system.tex	Wed Aug 18 17:15:51 1999 +0200
@@ -7,9 +7,7 @@
 
 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
 
-\author{{\em Markus Wenzel}\/\thanks{Section~\protect\ref{sec:info} was
-    written by Carsten Clasohm.  Section~\protect\ref{sec:browse} was
-    written by Stefan Berghofer.} \\
+\author{\emph{Markus Wenzel} and \emph{Stefan Berghofer} \\
   TU M\"unchen}
 
 \makeindex