# HG changeset patch # User wenzelm # Date 1015598012 -3600 # Node ID f27cc0a43feb714e432a7598d40a4ffb2ea1f3fe # Parent 69ab0e74ccdae24820c43b5b25bf15be48228425 tuned; diff -r 69ab0e74ccda -r f27cc0a43feb doc-src/System/basics.tex --- 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 diff -r 69ab0e74ccda -r f27cc0a43feb doc-src/System/misc.tex --- 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}. diff -r 69ab0e74ccda -r f27cc0a43feb doc-src/System/present.tex --- 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