diff -r 2c4b3b31a354 -r 1d7f8faaaea3 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/basics.tex	Mon Jan 12 15:47:43 1998 +0100
@@ -49,9 +49,8 @@
 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 just a few places, this is considered much more
-maintainable and user-friendly than ordinary shell environment
-variables.
+variables in just a few places, this is 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
@@ -121,7 +120,7 @@
 \end{itemize}
 
 \medskip The Isabelle settings scheme is basically quite simple, but
-non-trivial.  For debugging purposes, the generated environment may be
+non-trivial.  For debugging purposes, the resulting environment may be
 inspected with the \texttt{getenv} utility, see
 \S\ref{sec:tool-getenv}.
 
@@ -171,7 +170,8 @@
   
 \item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
   browser information (HTML and graph data) is stored (see also
-  \S\ref{sec:info}).
+  \S\ref{sec:info}).  The default value is
+  \texttt{\$ISABELLE_HOME_USER/browser_info}.
 
 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   none is given explicitely by the user --- e.g.\ when running
@@ -201,8 +201,7 @@
   
 \item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
   \texttt{isabelle} session derives an individual directory for
-  temporary files.  The default is somewhere in \texttt{/tmp}; this
-  should not need to be changed under normal circumstances.
+  temporary files.  The default is somewhere in \texttt{/tmp}.
   
 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
   actual user interface that the capital \texttt{Isabelle} should
@@ -250,7 +249,7 @@
 read-only. That is, the {\ML} world cannot be committed back into the
 logic image.  Otherwise, a writable session enables commits into
 either the input file, or into an alternative output heap file (in
-case this is given as the second argument).
+case this is given as the second argument on the command line).
 
 The read-write state of sessions is determined at startup only, it
 cannot be changed intermediately. Also note that heap images may
@@ -258,17 +257,17 @@
 themselves to dispose their heap files when they are no longer needed.
 
 \medskip The \texttt{-w} option makes the output heap file read-only
-after terminating the Isabelle session.  Thus subsequent invocations
-cause logic image to be read-only automatically.
+after terminating.  Thus subsequent invocations cause the logic image
+to be read-only automatically.
 
 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
 passed to the Isabelle session from the command line. Multiple
 \texttt{-e}'s are evaluated in order. Strange things may happen when
-errorneous {\ML} code is given. Also make sure that commands are
-terminated properly by semicolon.
+errorneous {\ML} code is given. Also make sure that the {\ML} commands
+are terminated properly by semicolon.
 
 \medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
-\texttt{use"ROOT.ML";} to the {\ML} session.
+``\texttt{use"ROOT.ML";}'' to the {\ML} session.
 
 \medskip The \texttt{-m} option adds identifiers of print modes to be
 made active for this session. Typically, this is used by some user
@@ -339,7 +338,7 @@
 \S\ref{sec:settings}.  The set of available tools is collected by
 isatool from the directories listed in the \texttt{ISABELLE_TOOLS}
 setting.  Do not try to call the scripts directly. Neither should you
-add the tools directories to your shell's search path.
+add the tool directories to your shell's search path.
 
 
 \medskip See chapter~\ref{ch:tools} for descriptions of most utilities