--- a/doc-src/System/basics.tex Fri Mar 08 11:43:01 2002 +0100
+++ b/doc-src/System/basics.tex Fri Mar 08 15:33:32 2002 +0100
@@ -4,10 +4,10 @@
\chapter{The Isabelle system environment}
This manual describes Isabelle together with related tools and user interfaces
-as seen from an outside (system oriented) view. See also the \emph{Isabelle
- Isar Reference Manual}~\cite{isabelle-isar-ref} and the \emph{Isabelle
- Reference Manual}~\cite{isabelle-ref} for the actual Isabelle commands and
-related functions.
+as seen from an outside (system oriented) view. See also the
+\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
+\emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
+commands and related functions.
\medskip The Isabelle system environment emerges from a few general concepts.
\begin{itemize}
@@ -26,7 +26,7 @@
Proof~General \cite{proofgeneral}.
\end{itemize}
-\medskip The beginning user would probably just run a standard user interface
+\medskip The beginning user would probably just run the default user interface
(by invoking the capital \texttt{Isabelle}). This assumes that the system has
already been installed, of course. In case you have to do this yourself, see
the \ttindex{INSTALL} file in the top-level directory of the distribution of
@@ -55,7 +55,7 @@
not required.}
-\subsection{Constructing the environment}
+\subsection{Building the environment}
Whenever any of the Isabelle executables is run, their settings environment is
put together as follows.
@@ -73,11 +73,11 @@
\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
with the auto-export option for variables enabled.
- This file typically contains a rather long list of shell variable
- assigments, thus providing the site-wide default settings. The Isabelle
- distribution already contains a global settings file with sensible defaults
- for most variables. When installing the system, only a few of these may have
- to be adapted (probably \texttt{ML_SYSTEM} etc.).
+ This file holds a rather long list of shell variable assigments, thus
+ providing the site-wide default settings. The Isabelle distribution already
+ contains a global settings file with sensible defaults for most variables.
+ When installing the system, only a few of these may have to be adapted
+ (probably \texttt{ML_SYSTEM} etc.).
\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
run in the same way as the site default settings. Note that the variable
@@ -290,8 +290,8 @@
\texttt{-r} option is given explicitely, then the session started will be
read-only. That is, the {\ML} world cannot be committed back into the image
file. Otherwise, a writable session enables commits into either the input
-file, or into an alternative output heap file (in case that is given as the
-second argument on the command line).
+file, or into another output heap file (if that 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 require considerable
@@ -333,7 +333,7 @@
\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
startup, instead of the primitive {\ML} top-level. The \texttt{-P} option
configures the top-level loop for interaction with the Proof~General user
-interface; do not enable this in ordinary sessions.
+interface; do not enable this in plain TTY sessions.
\subsection*{Examples}
@@ -381,10 +381,10 @@
Isabelle is a generic theorem prover, even w.r.t.\ its user interface. The
\ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
-uniform way for end-users to invoke a certain interface; which one to start
-actually is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
-Also note that the \texttt{install} utility provides some options to install
-desktop environment icons as well (see \S\ref{sec:tool-install}).
+uniform way for end-users to invoke a certain interface; which one to start is
+determined by the \settdx{ISABELLE_INTERFACE} setting variable. Also note
+that the \texttt{install} utility provides some options to install desktop
+environment icons as well (see \S\ref{sec:tool-install}).
An interface may be specified either by giving an identifier that the Isabelle
distribution knows about, or by specifying an actual path name (containing a
@@ -416,8 +416,8 @@
the Proof~General Lisp packages. There are some options available, such as
\texttt{-l} for passing the logic image to be used by default, or
\texttt{-m} to tune the standard print mode. The \texttt{-I} option allows
- to switch between the Isar and ML view, independently of the actual
- interface script being used.
+ to switch between the Isar and ML view, independently of the interface
+ script being used.
\medskip Note that the world may be also seen the other way round: Emacs may
be started first (with proper setup of Proof~General mode), and
--- a/doc-src/System/misc.tex Fri Mar 08 11:43:01 2002 +0100
+++ b/doc-src/System/misc.tex Fri Mar 08 15:33:32 2002 +0100
@@ -32,7 +32,7 @@
The \tooldx{doc} utility displays online documentation:
\begin{ttbox}
-Usage: isatool doc [DOC]
+Usage: doc [DOC]
View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
@@ -63,7 +63,7 @@
In the files or directories supplied as arguments, all occurrences of the
shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are
replaced with the corresponding full commands. The old versions of the files
-are renamed to have the suffix``~\verb'~~'''.
+are renamed to have the suffix ``\verb'~~'''.
\section{Getting logic images --- \texttt{isatool findlogics}}
@@ -71,7 +71,7 @@
The \tooldx{findlogics} utility traverses all directories specified in
\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is:
\begin{ttbox}
-Usage: isatool findlogics
+Usage: findlogics
Collect heap file names from ISABELLE_PATH.
\end{ttbox}
@@ -89,7 +89,7 @@
user-specific settings files --- can be inspected with the \tooldx{getenv}
utility:
\begin{ttbox}
-Usage: isatool getenv [OPTIONS] [VARNAMES ...]
+Usage: getenv [OPTIONS] [VARNAMES ...]
Options are:
-a display complete environment
@@ -182,8 +182,8 @@
-q quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your Isabelle
-project. For example, \texttt{isatool logo HOOL} creates
-\texttt{isabelle_hool.eps}.
+project. For example, \texttt{isatool logo Bali} creates
+\texttt{isabelle_bali.eps}.
\section{Isabelle's version of make --- \texttt{isatool make}}
@@ -192,7 +192,7 @@
The Isabelle \tooldx{make} utility is a very simple wrapper for
ordinary Unix \texttt{make}:
\begin{ttbox}
-Usage: isatool make [ARGS ...]
+Usage: make [ARGS ...]
Compile the logic in current directory using IsaMakefile.
ARGS are directly passed to the system make program.
@@ -215,7 +215,7 @@
\subsection*{Examples}
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
-object-logics as a model for your own developements. For example, see
+object-logics as a model for your own developments. For example, see
\texttt{src/FOL/IsaMakefile}.
--- a/doc-src/System/present.tex Fri Mar 08 11:43:01 2002 +0100
+++ b/doc-src/System/present.tex Fri Mar 08 15:33:32 2002 +0100
@@ -153,19 +153,16 @@
When no filename is specified, the browser automatically changes to the
directory \texttt{ISABELLE_BROWSER_INFO}.
-\medskip The \texttt{-d} option cases the source file (!)\ to be deleted after
-the browser terminates; this is mainly intended for detaching interactive
-graph views from a running Isabelle session.
+\medskip The \texttt{-d} option causes the source file (!)\ to be deleted
+after the browser terminates; this is mainly intended for detaching
+interactive graph views from a running Isabelle session.
The \texttt{-o} option indicates batch-mode operation, with the output written
to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as
well.
-\medskip The applet version of the browser can be invoked by opening the {\tt
- index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
-Web browser and selecting the version ``including theory graph browser''.
-There is also a link to the corresponding theory graph in every logic's {\tt
- index.html} file.
+\medskip The applet version of the browser is part of the standard WWW theory
+presentation, see the link ``theory dependencies'' within each session index.
\subsection{Using the graph browser}
@@ -282,8 +279,8 @@
The \tooldx{mkdir} utility prepares Isabelle session source directories,
including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML},
and a \texttt{document} directory with a minimal \texttt{root.tex} that is
-sufficient print all theories of the session (in the order of appearance); see
-\S\ref{sec:tool-document} for further information on Isabelle document
+sufficient to print all theories of the session (in the order of appearance);
+see \S\ref{sec:tool-document} for further information on Isabelle document
preparation. The usage of \texttt{isatool mkdir} is:
\begin{ttbox}
Usage: mkdir [OPTIONS] [LOGIC] NAME
@@ -343,8 +340,8 @@
\texttt{ROOT.ML} should be edited to load all required theories. Invoking
\texttt{isatool make} again would run the whole session, generating browser
information and the document automatically. The \texttt{IsaMakefile} is
-typically tuned manually later, e.g.\ adding actual source dependencies, or
-changing the options passed to \texttt{usedir}.
+typically tuned manually later, e.g.\ adding source dependencies, or changing
+the options passed to \texttt{usedir}.
\medskip Large projects may demand further sessions, potentially with separate
logic images being created. This usually requires manual editing of the
@@ -428,10 +425,10 @@
The \texttt{-g} option produces images of the theory dependency graph (cf.\
\S\ref{sec:browse}) for inclusion in the generated document, both as
\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
-In order to make this appear the final {\LaTeX} document one would typically
-say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
-file. (Omitting the file-name extension enables {\LaTeX} to select to correct
-version, either for the DVI or PDF output path.)
+To include this in the final {\LaTeX} document one could say
+\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting
+the file-name extension enables {\LaTeX} to select to correct version, either
+for the DVI or PDF output path).
\medskip The \texttt{-D} option causes the generated document sources
(including the user's template of \texttt{document/root.tex} etc.) to be
@@ -448,7 +445,7 @@
Manual}~\cite{isabelle-ref}.
\medskip The \texttt{-v} option causes additional information to be printed
-during while running the session, notably the location of prepared documents.
+while running the session, notably the location of prepared documents.
\medskip Any \texttt{usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend on
@@ -518,8 +515,8 @@
The {\LaTeX} versions of the theories require some macros defined in
\texttt{isabelle.sty} as distributed with Isabelle. Doing
-\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
-the underlying Isabelle \texttt{latex} utility already includes an appropriate
+\verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the
+underlying Isabelle \texttt{latex} utility already includes an appropriate
{\TeX} inputs path.
If the text contains any references to Isabelle symbols (such as