tuned;
authorwenzelm
Fri Mar 08 15:33:32 2002 +0100 (2002-03-08)
changeset 13047f27cc0a43feb
parent 13046 69ab0e74ccda
child 13048 8b2eb3b78cc3
tuned;
doc-src/System/basics.tex
doc-src/System/misc.tex
doc-src/System/present.tex
     1.1 --- a/doc-src/System/basics.tex	Fri Mar 08 11:43:01 2002 +0100
     1.2 +++ b/doc-src/System/basics.tex	Fri Mar 08 15:33:32 2002 +0100
     1.3 @@ -4,10 +4,10 @@
     1.4  \chapter{The Isabelle system environment}
     1.5  
     1.6  This manual describes Isabelle together with related tools and user interfaces
     1.7 -as seen from an outside (system oriented) view.  See also the \emph{Isabelle
     1.8 -  Isar Reference Manual}~\cite{isabelle-isar-ref} and the \emph{Isabelle
     1.9 -  Reference Manual}~\cite{isabelle-ref} for the actual Isabelle commands and
    1.10 -related functions.
    1.11 +as seen from an outside (system oriented) view.  See also the
    1.12 +\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
    1.13 +\emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
    1.14 +commands and related functions.
    1.15  
    1.16  \medskip The Isabelle system environment emerges from a few general concepts.
    1.17  \begin{itemize}
    1.18 @@ -26,7 +26,7 @@
    1.19    Proof~General \cite{proofgeneral}.
    1.20  \end{itemize}
    1.21  
    1.22 -\medskip The beginning user would probably just run a standard user interface
    1.23 +\medskip The beginning user would probably just run the default user interface
    1.24  (by invoking the capital \texttt{Isabelle}).  This assumes that the system has
    1.25  already been installed, of course.  In case you have to do this yourself, see
    1.26  the \ttindex{INSTALL} file in the top-level directory of the distribution of
    1.27 @@ -55,7 +55,7 @@
    1.28    not required.}
    1.29  
    1.30  
    1.31 -\subsection{Constructing the environment}
    1.32 +\subsection{Building the environment}
    1.33  
    1.34  Whenever any of the Isabelle executables is run, their settings environment is
    1.35  put together as follows.
    1.36 @@ -73,11 +73,11 @@
    1.37  \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
    1.38    with the auto-export option for variables enabled.
    1.39    
    1.40 -  This file typically contains a rather long list of shell variable
    1.41 -  assigments, thus providing the site-wide default settings.  The Isabelle
    1.42 -  distribution already contains a global settings file with sensible defaults
    1.43 -  for most variables. When installing the system, only a few of these may have
    1.44 -  to be adapted (probably \texttt{ML_SYSTEM} etc.).
    1.45 +  This file holds a rather long list of shell variable assigments, thus
    1.46 +  providing the site-wide default settings.  The Isabelle distribution already
    1.47 +  contains a global settings file with sensible defaults for most variables.
    1.48 +  When installing the system, only a few of these may have to be adapted
    1.49 +  (probably \texttt{ML_SYSTEM} etc.).
    1.50    
    1.51  \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
    1.52    run in the same way as the site default settings. Note that the variable
    1.53 @@ -290,8 +290,8 @@
    1.54  \texttt{-r} option is given explicitely, then the session started will be
    1.55  read-only.  That is, the {\ML} world cannot be committed back into the image
    1.56  file.  Otherwise, a writable session enables commits into either the input
    1.57 -file, or into an alternative output heap file (in case that is given as the
    1.58 -second argument on the command line).
    1.59 +file, or into another output heap file (if that is given as the second
    1.60 +argument on the command line).
    1.61  
    1.62  The read-write state of sessions is determined at startup only, it cannot be
    1.63  changed intermediately. Also note that heap images may require considerable
    1.64 @@ -333,7 +333,7 @@
    1.65  \medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
    1.66  startup, instead of the primitive {\ML} top-level.  The \texttt{-P} option
    1.67  configures the top-level loop for interaction with the Proof~General user
    1.68 -interface; do not enable this in ordinary sessions.
    1.69 +interface; do not enable this in plain TTY sessions.
    1.70  
    1.71  
    1.72  \subsection*{Examples}
    1.73 @@ -381,10 +381,10 @@
    1.74  
    1.75  Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
    1.76  \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
    1.77 -uniform way for end-users to invoke a certain interface; which one to start
    1.78 -actually is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
    1.79 -Also note that the \texttt{install} utility provides some options to install
    1.80 -desktop environment icons as well (see \S\ref{sec:tool-install}).
    1.81 +uniform way for end-users to invoke a certain interface; which one to start is
    1.82 +determined by the \settdx{ISABELLE_INTERFACE} setting variable.  Also note
    1.83 +that the \texttt{install} utility provides some options to install desktop
    1.84 +environment icons as well (see \S\ref{sec:tool-install}).
    1.85  
    1.86  An interface may be specified either by giving an identifier that the Isabelle
    1.87  distribution knows about, or by specifying an actual path name (containing a
    1.88 @@ -416,8 +416,8 @@
    1.89    the Proof~General Lisp packages.  There are some options available, such as
    1.90    \texttt{-l} for passing the logic image to be used by default, or
    1.91    \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
    1.92 -  to switch between the Isar and ML view, independently of the actual
    1.93 -  interface script being used.
    1.94 +  to switch between the Isar and ML view, independently of the interface
    1.95 +  script being used.
    1.96    
    1.97    \medskip Note that the world may be also seen the other way round: Emacs may
    1.98    be started first (with proper setup of Proof~General mode), and
     2.1 --- a/doc-src/System/misc.tex	Fri Mar 08 11:43:01 2002 +0100
     2.2 +++ b/doc-src/System/misc.tex	Fri Mar 08 15:33:32 2002 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4  
     2.5  The \tooldx{doc} utility displays online documentation:
     2.6  \begin{ttbox}
     2.7 -Usage: isatool doc [DOC]
     2.8 +Usage: doc [DOC]
     2.9  
    2.10    View Isabelle documentation DOC, or show list of available documents.
    2.11  \end{ttbox}
    2.12 @@ -63,7 +63,7 @@
    2.13  In the files or directories supplied as arguments, all occurrences of the
    2.14  shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are
    2.15  replaced with the corresponding full commands.  The old versions of the files
    2.16 -are renamed to have the suffix``~\verb'~~'''.
    2.17 +are renamed to have the suffix ``\verb'~~'''.
    2.18  
    2.19  
    2.20  \section{Getting logic images --- \texttt{isatool findlogics}}
    2.21 @@ -71,7 +71,7 @@
    2.22  The \tooldx{findlogics} utility traverses all directories specified in
    2.23  \texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is:
    2.24  \begin{ttbox}
    2.25 -Usage: isatool findlogics
    2.26 +Usage: findlogics
    2.27  
    2.28    Collect heap file names from ISABELLE_PATH.
    2.29  \end{ttbox}
    2.30 @@ -89,7 +89,7 @@
    2.31  user-specific settings files --- can be inspected with the \tooldx{getenv}
    2.32  utility:
    2.33  \begin{ttbox}
    2.34 -Usage: isatool getenv [OPTIONS] [VARNAMES ...]
    2.35 +Usage: getenv [OPTIONS] [VARNAMES ...]
    2.36  
    2.37    Options are:
    2.38      -a           display complete environment
    2.39 @@ -182,8 +182,8 @@
    2.40      -q           quiet mode
    2.41  \end{ttbox}
    2.42  You are encouraged to use this to create a derived logo for your Isabelle
    2.43 -project.  For example, \texttt{isatool logo HOOL} creates
    2.44 -\texttt{isabelle_hool.eps}.
    2.45 +project.  For example, \texttt{isatool logo Bali} creates
    2.46 +\texttt{isabelle_bali.eps}.
    2.47  
    2.48  
    2.49  \section{Isabelle's version of make --- \texttt{isatool make}}
    2.50 @@ -192,7 +192,7 @@
    2.51  The Isabelle \tooldx{make} utility is a very simple wrapper for
    2.52  ordinary Unix \texttt{make}:
    2.53  \begin{ttbox}
    2.54 -Usage: isatool make [ARGS ...]
    2.55 +Usage: make [ARGS ...]
    2.56  
    2.57    Compile the logic in current directory using IsaMakefile.
    2.58    ARGS are directly passed to the system make program.
    2.59 @@ -215,7 +215,7 @@
    2.60  \subsection*{Examples}
    2.61  
    2.62  Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
    2.63 -object-logics as a model for your own developements.  For example, see
    2.64 +object-logics as a model for your own developments.  For example, see
    2.65  \texttt{src/FOL/IsaMakefile}.
    2.66  
    2.67  
     3.1 --- a/doc-src/System/present.tex	Fri Mar 08 11:43:01 2002 +0100
     3.2 +++ b/doc-src/System/present.tex	Fri Mar 08 15:33:32 2002 +0100
     3.3 @@ -153,19 +153,16 @@
     3.4  When no filename is specified, the browser automatically changes to the
     3.5  directory \texttt{ISABELLE_BROWSER_INFO}.
     3.6  
     3.7 -\medskip The \texttt{-d} option cases the source file (!)\ to be deleted after
     3.8 -the browser terminates; this is mainly intended for detaching interactive
     3.9 -graph views from a running Isabelle session.
    3.10 +\medskip The \texttt{-d} option causes the source file (!)\ to be deleted
    3.11 +after the browser terminates; this is mainly intended for detaching
    3.12 +interactive graph views from a running Isabelle session.
    3.13  
    3.14  The \texttt{-o} option indicates batch-mode operation, with the output written
    3.15  to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as
    3.16  well.
    3.17  
    3.18 -\medskip The applet version of the browser can be invoked by opening the {\tt
    3.19 -  index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
    3.20 -Web browser and selecting the version ``including theory graph browser''.
    3.21 -There is also a link to the corresponding theory graph in every logic's {\tt
    3.22 -  index.html} file.
    3.23 +\medskip The applet version of the browser is part of the standard WWW theory
    3.24 +presentation, see the link ``theory dependencies'' within each session index.
    3.25  
    3.26  
    3.27  \subsection{Using the graph browser}
    3.28 @@ -282,8 +279,8 @@
    3.29  The \tooldx{mkdir} utility prepares Isabelle session source directories,
    3.30  including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML},
    3.31  and a \texttt{document} directory with a minimal \texttt{root.tex} that is
    3.32 -sufficient print all theories of the session (in the order of appearance); see
    3.33 -\S\ref{sec:tool-document} for further information on Isabelle document
    3.34 +sufficient to print all theories of the session (in the order of appearance);
    3.35 +see \S\ref{sec:tool-document} for further information on Isabelle document
    3.36  preparation.  The usage of \texttt{isatool mkdir} is:
    3.37  \begin{ttbox}
    3.38  Usage: mkdir [OPTIONS] [LOGIC] NAME
    3.39 @@ -343,8 +340,8 @@
    3.40  \texttt{ROOT.ML} should be edited to load all required theories.  Invoking
    3.41  \texttt{isatool make} again would run the whole session, generating browser
    3.42  information and the document automatically.  The \texttt{IsaMakefile} is
    3.43 -typically tuned manually later, e.g.\ adding actual source dependencies, or
    3.44 -changing the options passed to \texttt{usedir}.
    3.45 +typically tuned manually later, e.g.\ adding source dependencies, or changing
    3.46 +the options passed to \texttt{usedir}.
    3.47  
    3.48  \medskip Large projects may demand further sessions, potentially with separate
    3.49  logic images being created.  This usually requires manual editing of the
    3.50 @@ -428,10 +425,10 @@
    3.51  The \texttt{-g} option produces images of the theory dependency graph (cf.\ 
    3.52  \S\ref{sec:browse}) for inclusion in the generated document, both as
    3.53  \texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
    3.54 -In order to make this appear the final {\LaTeX} document one would typically
    3.55 -say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex}
    3.56 -file.  (Omitting the file-name extension enables {\LaTeX} to select to correct
    3.57 -version, either for the DVI or PDF output path.)
    3.58 +To include this in the final {\LaTeX} document one could say
    3.59 +\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting
    3.60 +the file-name extension enables {\LaTeX} to select to correct version, either
    3.61 +for the DVI or PDF output path).
    3.62  
    3.63  \medskip The \texttt{-D} option causes the generated document sources
    3.64  (including the user's template of \texttt{document/root.tex} etc.) to be
    3.65 @@ -448,7 +445,7 @@
    3.66    Manual}~\cite{isabelle-ref}.
    3.67  
    3.68  \medskip The \texttt{-v} option causes additional information to be printed
    3.69 -during while running the session, notably the location of prepared documents.
    3.70 +while running the session, notably the location of prepared documents.
    3.71  
    3.72  \medskip Any \texttt{usedir} session is named by some \emph{session
    3.73    identifier}. These accumulate, documenting the way sessions depend on
    3.74 @@ -518,8 +515,8 @@
    3.75  
    3.76  The {\LaTeX} versions of the theories require some macros defined in
    3.77  \texttt{isabelle.sty} as distributed with Isabelle.  Doing
    3.78 -\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
    3.79 -the underlying Isabelle \texttt{latex} utility already includes an appropriate
    3.80 +\verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the
    3.81 +underlying Isabelle \texttt{latex} utility already includes an appropriate
    3.82  {\TeX} inputs path.
    3.83  
    3.84  If the text contains any references to Isabelle symbols (such as