preliminary!

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/basics.tex	Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,229 @@
+
+% $Id$
+
+\chapter{Basic concepts}
+
+The \emph{Isabelle System Manual} describes Isabelle together with its
+related tools and user interfaces --- as seen from an outside
+(operating system oriented) view.  On the other hand, see
+\emph{Isabelle Reference} for all internal {\ML} level user commands.
+
+\medskip The Isabelle system level environment is based on a few
+generic concepts that are simple, but non-trivial:
+\begin{itemize}
+\item The \emph{Isabelle settings mechanism}, which provides
+  environment values to all Isabelle programs (including tools and
+  user interfaces).
+\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic
+  sessions, both interactively or in batch mode. In particular,
+  \texttt{isabelle} abstracts over the invocation of the actual {\ML}
+  system to be used.
+\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which
+  provides a generic startup platform for miscellaneous utilities.
+  Thus tools automatically benefit from the settings mechanism.
+  Furthermore, the shell's search path is kept clean from many small
+  programs.
+\item The \emph{Isabelle interface wrapper}
+  (\ttindex{Isabelle}\footnote{Note the capital \texttt{I}!}), which
+  provides some abstraction over the actual user interface to be used
+  (this may include third-party ones).
+\end{itemize}
+
+\medskip The beginning user would probably just run one of the
+interfaces (by invoking the capital \texttt{Isabelle}), and maybe some
+basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}).  This
+assumes that the system has already been installed properly, of
+course.\footnote{In case you have to do this yourself from scratch,
+  see the \ttindex{INSTALL} file in the top-level directory of the
+  distribution. The information provided there should be sufficient as
+  a start.}
+
+
+\section{Isabelle settings} \label{sec:settings}
+
+The Isabelle system heavily depends on the \emph{settings
+  mechanism}\indexbold{settings}. Basically, this is just a collection
+of environment variables, e.g.\ \texttt{ISABELLE_HOME},
+\texttt{ML_SYSTEM}, \texttt{ML_HOME}.  These variables are \emph{not}
+intended to be set directly from the shell!
+
+Isabelle employs a somewhat more sophisticated scheme of
+\emph{settings files} --- one for site-wide defaults, another for
+optional user-specific modifications.  With all configuration
+variables in only one or two places, this is considered much more
+maintainable and user-friendly than ordinary shell environment
+variables.
+
+In particular, we avoid the typical situation where prospective users
+of a software package are told to put this and that in their shell
+startup scripts. Isabelle requires none such administrative chores of
+its end-users --- the executables can be run straight away. Usually,
+users would want to put the Isabelle \texttt{bin} directory into their
+shell's search path, of course.
+
+
+\subsection{Building the environment}
+
+The environment that all Isabelle programs are run in is built as
+follows:
+
+\begin{enumerate}
+\item The special variable \ttindex{ISABELLE_HOME} is determined
+  automatically from the location of the binary that has been run
+  (e.g.\ \texttt{isabelle}).
+  
+  You should not try to set \texttt{ISABELLE_HOME} manually. Also note
+  that the Isabelle executables have to be run from their original
+  location in the distribution directory --- copying or linking them
+  somewhere else just won't work!
+  
+\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a GNU
+  bash script with the variable auto-export option enabled.
+  
+  The file typically contains a rather long list of assigments
+  \texttt{FOO="bar"}, thus providing the site default settings. The
+  Isabelle distribution already contains a global settings file with
+  sensible defaults. When installing the system, only a few of these
+  have to be adapted (most likely \texttt{ML_SYSTEM} and friends).
+  
+\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
+  exists) is run the same way as the site default settings. The
+  variable \texttt{ISABELLE_HOME_USER} has already been set before ---
+  usually to \texttt{\~\relax/isabelle}.
+  
+  Thus individual users may override the site-wide defaults. See also
+  file \texttt{etc/user-settings.sample} in the distribution.
+  Typically, user settings are a few lines only, just containing the
+  assigments that are really required.  One should definitely
+  \emph{not} start with a full copy the central
+  \texttt{\$ISABELLE_HOME/etc/settings}. This may cause severe
+  maintainance problems later, when the Isabelle installation is
+  updated or changed otherwise.
+
+\end{enumerate}
+
+Note that settings files are actually bash scripts. So one may use
+complex shell commands, e.g.\ \texttt{if} or \texttt{case} statements
+to set variables depending on the system architecture or other
+environment variables. Such advanced features should be added only
+with great care, though. In particular, external environment
+references should be kept at a minimum.
+
+\medskip A few variables are somewhat:
+\begin{itemize}
+\item \ttindex{ISABELLE} and \ttindex{ISATOOL} are set automatically
+  to the absolute path names of the \texttt{isabelle} and
+  \texttt{isatool} executables, respectively.
+  
+\item \ttindex{ISABELLE_PATH} and \ttindex{ISABELLE_OUTPUT} will have
+  the {\ML} system identifier (as specified by \texttt{ML_SYSTEM})
+  automatically appended to their values.
+\end{itemize}
+
+\medskip The Isabelle settings scheme is basically quite simple, but
+non-trivial.  For debugging purposes, the generated environment may be
+inspected with the \texttt{getenv} Isabelle tool, see
+\S\ref{sec:tool-getenv}.
+
+
+\subsection{Common variables}
+
+Below is a reference of common Isabelle settings variables. The list
+is somewhat open-ended, in particular, third-party utilities or
+interfaces may add their own selection.
+
+\begin{ttdescription}
+\item[FIXME] FIXME
+\end{ttdescription}
+
+
+\section{Isabelle proper --- \texttt{isabelle}}
+
+The \ttindex{isabelle} executable runs logic sessions --- either
+interactively or in batch mode. It provides an abstraction over the
+underlying {\ML} system, and over the actual heap file locations. The usage is:
+\begin{ttbox}
+Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
+
+  Options are:
+    -e MLTEXT    pass MLTEXT to the ML session
+    -m MODE      add print mode for output
+    -q           non-interactive session
+    -r           open heap file read-only
+
+  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
+  These are either names to be searched in the Isabelle path, or actual
+  file names (then containing at least one /).
+  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
+\end{ttbox}
+Input files without path specifications are looked up in the
+\texttt{ISABELLE_PATH} setting, which may consist of multiple
+components separated by colons --- these are tried in the given order.
+Short output names are relative to the directory specified by
+\texttt{ISABELLE_OUTPUT} setting.  In any case, actual file locations
+can be given by including at least one \texttt{/} (use \texttt{./} to
+refer to the current directory).
+
+If the input heap file is not writable, or the \texttt{-r} option is
+given explicitely, the session will be read-only. That is, the {\ML}
+world cannot be committed back into the logic image.  A writable
+session enables commits into either the input file, or into an
+alternative output heap file which may be given as the second
+argument.
+
+The read-write state of sessions is determined at startup only, it
+cannot be changed intermediately. Also note that heap images may
+require considerable amounts of disk space. Users are responsible
+themselves to dispose no longer needed heap files.
+
+
+\subsection*{Options}
+
+Using \texttt{-e} one may pass {\ML} code to the Isabelle session from
+the command line. Multiple \texttt{-e}'s are evaluated in the given
+order.
+
+The \texttt{-m} option addes print mode identifiers to be made active
+for this session. Typically this is used by some user interface to
+enable output of mathematical symbols from a special screen font, for
+example (see also \S\ref{sec:fonts} about fonts and the \emph{Isabelle
+  Reference Manual} about print modes in general).
+
+Isabelle normally enters an interactice {\ML} top-level loop (after
+processing the \texttt{-e} texts). The \texttt{-q} option inhibits
+this, providing a pure batch mode facility.
+
+
+\subsection*{Examples}
+
+Run an interactive session of the default object-logic:
+\begin{ttbox}
+isabelle
+\end{ttbox}
+Usually, this refers to one of the standard logic images, which are
+read-only by default.
+
+Run a writable session, based on \texttt{FOL}, but output to
+\texttt{Foo} (in the directory specified by the
+\texttt{ISABELLE_OUTPUT} setting):
+\begin{ttbox}
+isabelle FOL Foo
+\end{ttbox}
+Ending this session normally (e.g.\ by typing control-D), dumps the
+whole {\ML} system state into \texttt{Foo}. Be prepared for several
+megabytes!
+
+The \texttt{Foo} session may be continued (writably!) at exactly the
+same point as follows:
+\begin{ttbox}
+isabelle Foo
+\end{ttbox}
+
+\medskip This is a simple batch mode example, printing a certain
+theorem of \texttt{FOL}:
+\begin{ttbox}
+isabelle -e "prth allE;" -q -r FOL
+\end{ttbox}
+Note that the output text will be usually interspered with some
+garbage produced by the {\ML} compiler.
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/fonts.tex	Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,21 @@
+
+\chapter{Fonts and character encodings}
+
+\section{ --- \texttt{isatool installfonts}}
+
+\begin{ttbox}
+Usage: isatool installfonts
+
+  Install the isabelle fonts into your X11 server.
+  (May be savely called repeatedly.)
+\end{ttbox}
+
+
+\section{ --- \texttt{isatool symbolinput}}
+
+
+%FIXME not yet
+%\section{ --- \texttt{isatool showsymbols}}
+%
+%\begin{ttbox}
+%\end{ttbox}

--- a/doc-src/System/html.tex	Wed May 14 18:42:09 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-\chapter{Generating HTML documents} \label{html}
-\index{HTML|bold} 
-
-Isabelle is able to make HTML documents that show a theory's
-definition, the theorems proved in its ML file and the relationship
-with its ancestors and descendants. HTML stands for Hypertext Markup
-Language and is used in the World Wide Web to represent text
-containing images and links to other documents. Web browsers like
-{\tt xmosaic} or {\tt netscape} are used to view these documents.
-
-Besides the three HTML files that are made for every theory
-(definition and theorems, ancestors, descendants), 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.
-
-To make HTML files for logics that are part of the Isabelle
-distribution, simply set the shell environment variable {\tt
-MAKE_HTML} before compiling a logic. This works for single logics as
-well as for the shell script {\tt make-all} (see
-\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
-{\tt csh} style shell, the following commands can be used:
-
-\begin{ttbox}
-cd FOL
-setenv MAKE_HTML
-make
-\end{ttbox}
-
-The databases made this way do not differ from the ones made with an
-unset {\tt MAKE_HTML}; in particular no HTML files are written if the
-database is used to manually load a theory.
-
-As you will see below, the HTML generation is controlled by a boolean
-reference variable. If you want to make databases which define this
-variable's value as {\tt true} and where therefore HTML files are
-written each time {\tt use_thy} is invoked, you have to set {\tt
-MAKE_HTML} to ``{\tt true}'':
-
-\begin{ttbox}
-cd FOL
-setenv MAKE_HTML true
-make
-\end{ttbox}
-
-All theories loaded from within the {\tt FOL} database and all
-databases derived from it will now cause HTML files to be written.
-This behaviour can be changed by assigning a value of {\tt false} to
-the boolean reference variable {\tt make_html}. Be careful when making
-such databases publicly available since it means that your users will
-generate HTML files though they might not intend to do so.
-
-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.
-
-The entry point to all logics is the {\tt index.html} file located in
-Isabelle's main directory. You can also access a HTML version of the
-distribution package at
-
-\begin{ttbox}
-http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
-\end{ttbox}
-
-
-\section*{Manual HTML generation}
-
-To manually control the generation of HTML files the following
-commands and reference variables are used:
-
-\begin{ttbox}
-init_html   : unit -> unit
-make_html   : bool ref
-finish_html : unit -> unit
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{init_html}]
-activates the HTML facility. It stores the current working directory
-as the place where the {\tt index.html} file for all theories loaded
-afterwards will be stored.
-
-\item[\ttindexbold{make_html}]
-is a boolean reference variable read by {\tt use_thy} and other
-functions to decide whether HTML files should be made. After you have
-used {\tt init_html} you can manually change {\tt make_html}'s value
-to temporarily disable HTML generation.
-
-\item[\ttindexbold{finish_html}]
-has to be called after all theories have been read that should be
-listed in the current {\tt index.html} file. It reads a temporary
-file with information about the theories read since the last use of
-{\tt init_html} and makes the {\tt index.html} file. If {\tt
-make_html} is {\tt false} nothing is done.
-
-The indexes made by this function also contain a link to the {\tt
-README} file if there exists one in the directory where the index is
-stored. If there's a {\tt README.html} file it is used instead of
-{\tt README}.
-
-\end{ttdescription}
-
-The above functions could be used in the following way:
-
-\begin{ttbox}
-init_html();
-{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
-use_thy "List";
-\dots
-finish_html();
-\end{ttbox}
-
-Please note that HTML files are made only for those theories that are
-read while {\tt make_html} is {\tt true}. These files may contain
-links to theories that were read with a {\tt false} {\tt make_html}
-and therefore point to non-existing files.
-
-
-\section*{Extending or adding a logic}
-
-If you add a new subdirectory to Isabelle's logics (or add a completly
-new logic), you would have to call {\tt init_html} at the start of every
-directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
-it. This is automatically done if you use
-
-\begin{ttbox}\index{*use_dir}
-use_dir : string -> unit
-\end{ttbox}
-
-This function takes a path as its parameter, changes the working
-directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
-executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
-index.html} file written in this directory will be automatically
-linked to the first index found in the (recursively searched)
-superdirectories.
-
-Instead of adding something like
-
-\begin{ttbox}
-use"ex/ROOT.ML";
-\end{ttbox}
-
-to the logic's makefile you have to use this:
-
-\begin{ttbox}
-use_dir"ex";
-\end{ttbox}
-
-Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
-{\tt true} the generation of HTML files depends on the value this
-reference variable has. It can either be inherited from the used \ML{}
-database or set in the makefile before {\tt use_dir} is invoked,
-e.g. to set it's value according to the environment variable {\tt
-MAKE_HTML}.
-
-The generated HTML files contain all theorems that were proved in the
-theory's \ML{} file 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}
-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. If {\tt make_html} is {\tt false} nothing
-is done.
-
-
-\section*{Using someone else's database}
-
-To make them independent from their storage place, the HTML files only
-contain relative paths which are derived from absolute ones like the
-current working directory, {\tt gif_path} or {\tt base_path}. The
-latter two are reference variables which are initialized at the time
-when the {\tt Pure} database is made. Because you need write access
-for the current directory to make HTML files and therefore (probably)
-generate them in your home directory, the absolute {\tt base_path} is
-not correct if you use someone else's database or a database derived
-from it.
-
-In that case you first should set {\tt base_path} to the value of {\em
-your} Isabelle main directory, i.e. the directory that contains the
-subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
-your own logics are stored. If you do not do this, the generated HTML
-files will still be usable but may contain incomplete titles and lack
-some hypertext links.
-
-It's also a good idea to set {\tt gif_path} which points to the
-directory containing two GIF images used in the HTML
-documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
-main directory. While its value in general is still valid, your HTML
-files would depend on files not owned by you. This prevents you from
-changing the location of the HTML files (as they contain relative
-paths) and also causes trouble if the database's maker (re)moves the
-GIFs.
-
-Here's what you should do before invoking {\tt init_html} using
-someone else's \ML{} database:
-
-\begin{ttbox}
-base_path := "/home/smith/isabelle";
-gif_path := "/home/smith/isabelle/Tools";
-init_html();
-\dots
-\end{ttbox}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/misc.tex	Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,111 @@
+
+% $Id$
+
+\chapter{Miscellaneous tools}
+
+
+\section{Inspecting the settings environment -- \texttt{isatool getenv}}
+\label{sec:tool-getenv}
+
+The Isabelle settings environment --- as provided by the site-default
+and user-specific settings files --- can be inspected with the
+\tooldx{getenv} utility:
+\begin{ttbox}
+Usage: isatool getenv [OPTIONS] [VARNAMES ...]
+
+  Options are:
+    -a           display complete environment
+    -b           print values only (doesn't work for -a)
+
+  Get value of VARNAMES from the Isabelle settings.
+\end{ttbox}
+
+With the \texttt{-a} option, one may inspect the full process
+environment that Isabelle related programs are run in. This usually
+contains much more variables than are actually Isabelle settings.
+
+Unless the \texttt{-b} option is given, the output is a list of lines
+of the form $varname\mathtt{=}value$.
+
+
+\subsection*{Examples}
+
+Get the {\ML} system identifier and the location where the compiler
+binaries are supposed to be installed as follows:
+\begin{ttbox}
+isatool getenv ML_SYSTEM ML_HOME
+{\out ML_HOME=/usr/local/sml109.27/bin}
+{\out ML_SYSTEM=smlnj-1.09}
+\end{ttbox}
+
+This one peeks at the search path that \texttt{isabelle} uses to
+locate logic images:
+\begin{ttbox}
+isatool getenv -b ISABELLE_PATH
+{\out /home/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
+\end{ttbox}
+We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
+prefix.  The value above is what became of the following assignment in
+the default settings file:
+\begin{ttbox}
+ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
+\end{ttbox}
+Note how \texttt{\$ML_SYSTEM} got appended automatically to each path
+component. This is a special feature of \texttt{ISABELLE_PATH} (and
+also of \texttt{ISABELLE_OUTPUT}).
+
+\section{Get logic images --- \texttt{isatool findlogics}}
+
+\begin{ttbox}
+Usage: isatool findlogics
+
+  Collect heap file names from ISABELLE_PATH.
+\end{ttbox}
+
+\section{Isabelle's version of make --- \texttt{isatool make}}
+
+\begin{ttbox}
+Usage: isatool make [ARGS ...]
+
+  Compiles logic in current directory using IsaMakefile.
+  ARGS are directly passed to the system make program.
+\end{ttbox}
+
+
+\section{ --- \texttt{isatool usedir}}
+
+\begin{ttbox}
+Usage: isatool usedir LOGIC NAME
+
+  Options are:
+    -b           build mode (output heap image, use dir ".")
+    -g BOOL      generate theory graph data (default false)
+    -h BOOL      generate theory HTML data (default false)
+    -s NAME      override session NAME
+
+  Build object-logic or run examples. Also creates browsing
+  information (HTML etc.) according to settings.
+\end{ttbox}
+
+
+\section{ --- \texttt{isatool doc}}
+
+\begin{ttbox}
+Usage: isatool doc [DOC]
+
+  View Isabelle documentation DOC, or show list of available documents.
+\end{ttbox}
+
+
+\section{ --- \texttt{isatool expandshort}}
+
+\begin{ttbox}
+Usage: expandshort [FILES ...]
+
+  Expand shorthand goal commands in FILES.  Also contracts uses of
+  resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
+  1-element lists; furthermore expands tabs, since they are now
+  forbidden in ML string constants.
+
+  Renames old versions of FILES by appending "~~".
+\end{ttbox}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/present.tex	Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,214 @@
+
+\chapter{Presenting theories}
+
+\section{Generating HTML documents} \label{sec:html}
+\index{HTML|bold} 
+
+Isabelle is able to make HTML documents that show a theory's
+definition, the theorems proved in its ML file and the relationship
+with its ancestors and descendants. HTML stands for Hypertext Markup
+Language and is used in the World Wide Web to represent text
+containing images and links to other documents. Web browsers like
+{\tt xmosaic} or {\tt netscape} are used to view these documents.
+
+Besides the three HTML files that are made for every theory
+(definition and theorems, ancestors, descendants), 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.
+
+To make HTML files for logics that are part of the Isabelle
+distribution, simply set the shell environment variable {\tt
+MAKE_HTML} before compiling a logic. This works for single logics as
+well as for the shell script {\tt make-all} (see
+\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
+{\tt csh} style shell, the following commands can be used:
+
+\begin{ttbox}
+cd FOL
+setenv MAKE_HTML
+make
+\end{ttbox}
+
+The databases made this way do not differ from the ones made with an
+unset {\tt MAKE_HTML}; in particular no HTML files are written if the
+database is used to manually load a theory.
+
+As you will see below, the HTML generation is controlled by a boolean
+reference variable. If you want to make databases which define this
+variable's value as {\tt true} and where therefore HTML files are
+written each time {\tt use_thy} is invoked, you have to set {\tt
+MAKE_HTML} to ``{\tt true}'':
+
+\begin{ttbox}
+cd FOL
+setenv MAKE_HTML true
+make
+\end{ttbox}
+
+All theories loaded from within the {\tt FOL} database and all
+databases derived from it will now cause HTML files to be written.
+This behaviour can be changed by assigning a value of {\tt false} to
+the boolean reference variable {\tt make_html}. Be careful when making
+such databases publicly available since it means that your users will
+generate HTML files though they might not intend to do so.
+
+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.
+
+The entry point to all logics is the {\tt index.html} file located in
+Isabelle's main directory. You can also access a HTML version of the
+distribution package at
+
+\begin{ttbox}
+http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
+\end{ttbox}
+
+
+\section*{Manual HTML generation}
+
+To manually control the generation of HTML files the following
+commands and reference variables are used:
+
+\begin{ttbox}
+init_html   : unit -> unit
+make_html   : bool ref
+finish_html : unit -> unit
+\end{ttbox}
+
+\begin{ttdescription}
+\item[\ttindexbold{init_html}]
+activates the HTML facility. It stores the current working directory
+as the place where the {\tt index.html} file for all theories loaded
+afterwards will be stored.
+
+\item[\ttindexbold{make_html}]
+is a boolean reference variable read by {\tt use_thy} and other
+functions to decide whether HTML files should be made. After you have
+used {\tt init_html} you can manually change {\tt make_html}'s value
+to temporarily disable HTML generation.
+
+\item[\ttindexbold{finish_html}]
+has to be called after all theories have been read that should be
+listed in the current {\tt index.html} file. It reads a temporary
+file with information about the theories read since the last use of
+{\tt init_html} and makes the {\tt index.html} file. If {\tt
+make_html} is {\tt false} nothing is done.
+
+The indexes made by this function also contain a link to the {\tt
+README} file if there exists one in the directory where the index is
+stored. If there's a {\tt README.html} file it is used instead of
+{\tt README}.
+
+\end{ttdescription}
+
+The above functions could be used in the following way:
+
+\begin{ttbox}
+init_html();
+{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
+use_thy "List";
+\dots
+finish_html();
+\end{ttbox}
+
+Please note that HTML files are made only for those theories that are
+read while {\tt make_html} is {\tt true}. These files may contain
+links to theories that were read with a {\tt false} {\tt make_html}
+and therefore point to non-existing files.
+
+
+\section*{Extending or adding a logic}
+
+If you add a new subdirectory to Isabelle's logics (or add a completly
+new logic), you would have to call {\tt init_html} at the start of every
+directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
+it. This is automatically done if you use
+
+\begin{ttbox}\index{*use_dir}
+use_dir : string -> unit
+\end{ttbox}
+
+This function takes a path as its parameter, changes the working
+directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
+executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
+index.html} file written in this directory will be automatically
+linked to the first index found in the (recursively searched)
+superdirectories.
+
+Instead of adding something like
+
+\begin{ttbox}
+use"ex/ROOT.ML";
+\end{ttbox}
+
+to the logic's makefile you have to use this:
+
+\begin{ttbox}
+use_dir"ex";
+\end{ttbox}
+
+Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
+{\tt true} the generation of HTML files depends on the value this
+reference variable has. It can either be inherited from the used \ML{}
+database or set in the makefile before {\tt use_dir} is invoked,
+e.g. to set it's value according to the environment variable {\tt
+MAKE_HTML}.
+
+The generated HTML files contain all theorems that were proved in the
+theory's \ML{} file 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}
+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. If {\tt make_html} is {\tt false} nothing
+is done.
+
+
+\section*{Using someone else's database}
+
+To make them independent from their storage place, the HTML files only
+contain relative paths which are derived from absolute ones like the
+current working directory, {\tt gif_path} or {\tt base_path}. The
+latter two are reference variables which are initialized at the time
+when the {\tt Pure} database is made. Because you need write access
+for the current directory to make HTML files and therefore (probably)
+generate them in your home directory, the absolute {\tt base_path} is
+not correct if you use someone else's database or a database derived
+from it.
+
+In that case you first should set {\tt base_path} to the value of {\em
+your} Isabelle main directory, i.e. the directory that contains the
+subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
+your own logics are stored. If you do not do this, the generated HTML
+files will still be usable but may contain incomplete titles and lack
+some hypertext links.
+
+It's also a good idea to set {\tt gif_path} which points to the
+directory containing two GIF images used in the HTML
+documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
+main directory. While its value in general is still valid, your HTML
+files would depend on files not owned by you. This prevents you from
+changing the location of the HTML files (as they contain relative
+paths) and also causes trouble if the database's maker (re)moves the
+GIFs.
+
+Here's what you should do before invoking {\tt init_html} using
+someone else's \ML{} database:
+
+\begin{ttbox}
+base_path := "/home/smith/isabelle";
+gif_path := "/home/smith/isabelle/Tools";
+init_html();
+\dots
+\end{ttbox}

--- a/doc-src/System/system.ind	Wed May 14 18:42:09 1997 +0200
+++ b/doc-src/System/system.ind	Wed May 14 19:27:21 1997 +0200
@@ -1,25 +1,42 @@
 \begin{theindex}
 
-  \item browser, \bold{5}
+  \item browser, \bold{14}
 
   \indexspace
 
-  \item {\tt finish_html}, \bold{2}
+  \item {\tt finish_html}, \bold{11}
+
+  \indexspace
+
+  \item {\tt getenv} tool, 5
+
+  \indexspace
+
+  \item HTML, \bold{10}
 
   \indexspace
 
-  \item HTML, \bold{1}
-
-  \indexspace
-
-  \item {\tt init_html}, \bold{2}
+  \item {\tt init_html}, \bold{11}
+  \item {\tt INSTALL}, 1
+  \item {\tt ISABELLE}, 3
+  \item {\tt Isabelle}, 1
+  \item {\tt isabelle}, 1, 3
+  \item {\tt ISABELLE_HOME}, 2
+  \item {\tt ISABELLE_OUTPUT}, 3
+  \item {\tt ISABELLE_PATH}, 3
+  \item {\tt ISATOOL}, 3
+  \item {\tt isatool}, 1
 
   \indexspace
 
-  \item {\tt make_html}, \bold{2}
+  \item {\tt make_html}, \bold{11}
 
   \indexspace
 
-  \item {\tt use_dir}, 3
+  \item settings, \bold{1}
+
+  \indexspace
+
+  \item {\tt use_dir}, 12
 
 \end{theindex}

--- a/doc-src/System/system.tex	Wed May 14 18:42:09 1997 +0200
+++ b/doc-src/System/system.tex	Wed May 14 19:27:21 1997 +0200
@@ -17,7 +17,7 @@
         With Contributions by Tobias Nipkow and Markus Wenzel%
         \thanks{Chapter~\protect\ref{html} was written by Carsten
           Clasohm.  Chapter~\protect\ref{browse} was written by Stefan
-          Berghofer. Some other parts are by Markus Wenzel.}}
+          Berghofer. Other parts are by Markus Wenzel.}}
 
 \makeindex
 
@@ -35,7 +35,10 @@
 
 %\include{introduction}
 
-\include{html}
+\include{basics}
+\include{misc}
+\include{fonts}
+\include{present}
 \include{browse}
 
 %\begingroup