--- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 09 14:01:09 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 09 14:01:13 2002 +0100
@@ -315,10 +315,10 @@
both to the machine and human readers at the same time. Thus
marginal comments and explanations may be kept at a minimum. Even
without proper coverage of human-readable proofs, Isabelle document
- is very useful to produce formally derived texts. Unstructured
- proof scripts given here may be just ignored by readers, or
- intentionally suppressed from the text by the writer (see also
- \S\ref{sec:doc-prep-suppress}).
+ preparation is very useful to produce formally derived texts.
+ Unstructured proof scripts given here may be just ignored by
+ readers, or intentionally suppressed from the text by the writer
+ (see also \S\ref{sec:doc-prep-suppress}).
\medskip The Isabelle document preparation system essentially acts
as a front-end to {\LaTeX}. After checking specifications and
@@ -337,11 +337,11 @@
In contrast to the highly interactive mode of Isabelle/Isar theory
development, the document preparation stage essentially works in
batch-mode. An Isabelle \bfindex{session} consists of a collection
- of theory source files that contribute to a single output document
- eventually. Each session is derived from a single parent one,
- usually an object-logic image like \texttt{HOL}. This results in an
- overall tree structure, which is reflected by the output location in
- the file system (usually rooted at \verb,~/isabelle/browser_info,).
+ of theory source files that contribute to an output document
+ eventually. Each session is derived from a single parent, usually
+ an object-logic image like \texttt{HOL}. This results in an overall
+ tree structure, which is reflected by the output location in the
+ file system (usually rooted at \verb,~/isabelle/browser_info,).
\medskip Here is the canonical arrangement of sources of a session
called \texttt{MySession}:
@@ -368,11 +368,10 @@
\verb,\input{session}, in \texttt{root.tex} does the job in most
situations.
- \item \texttt{IsaMakefile} outside of the directory
- \texttt{MySession} holds appropriate dependencies and invocations of
- Isabelle tools to control the batch job. In fact, several sessions
- may be controlled by the same \texttt{IsaMakefile}. See also
- \cite{isabelle-sys} for further details, especially on
+ \item \texttt{IsaMakefile} holds appropriate dependencies and
+ invocations of Isabelle tools to control the batch job. In fact,
+ several sessions may be controlled by the same \texttt{IsaMakefile}.
+ See also \cite{isabelle-sys} for further details, especially on
\texttt{isatool usedir} and \texttt{isatool make}.
\end{itemize}
@@ -403,7 +402,7 @@
\medskip One may now start to populate the directory
\texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
- accordingly. \texttt{MySession/document/root.tex} should be also
+ accordingly. \texttt{MySession/document/root.tex} should also be
adapted at some point; the default version is mostly
self-explanatory. Note that \verb,\isabellestyle, enables
fine-tuning of the general appearance of characters and mathematical
@@ -439,7 +438,7 @@
The large-scale structure of Isabelle documents follows existing
{\LaTeX} conventions, with chapters, sections, subsubsections etc.
The Isar language includes separate \bfindex{markup commands}, which
- do not effect the formal content of a theory (or proof), but result
+ do not affect the formal meaning of a theory (or proof), but result
in corresponding {\LaTeX} elements.
There are separate markup commands depending on the textual context:
@@ -537,7 +536,7 @@
serve technical purposes to mark certain oddities in the raw input
text. In contrast, \bfindex{formal comments} are portions of text
that are associated with formal Isabelle/Isar commands
- (\bfindex{marginal comments}), or as stanalone paragraphs within a
+ (\bfindex{marginal comments}), or as standalone paragraphs within a
theory or proof context (\bfindex{text blocks}).
\medskip Marginal comments are part of each command's concrete
@@ -666,7 +665,7 @@
(cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
mathematical notation in both the formal and informal parts of the
document very easily. Manual {\LaTeX} code would leave more control
- over the type-setting, but is also slightly more tedious.%
+ over the typesetting, but is also slightly more tedious.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -677,7 +676,7 @@
\begin{isamarkuptext}%
As has been pointed out before (\S\ref{sec:syntax-symbols}),
Isabelle symbols are the smallest syntactic entities --- a
- straight-forward generalization of ASCII characters. While Isabelle
+ straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents show canonical glyphs for certain
standard symbols \cite[appendix~A]{isabelle-sys}.
@@ -714,7 +713,7 @@
example, \verb,\isabellestyle{it}, uses the italics text style to
mimic the general appearance of the {\LaTeX} math mode; double
quotes are not printed at all. The resulting quality of
- type-setting is quite good, so this should usually be the default
+ typesetting is quite good, so this should usually be the default
style for real production work that gets distributed to a broader
audience.%
\end{isamarkuptext}%
@@ -746,7 +745,7 @@
no_document use_thy "T";
\end{verbatim}
- \medskip Theory output may be also suppressed in smaller portions.
+ \medskip Theory output may also be suppressed in smaller portions.
For example, research articles, or slides usually do not include the
formal content in full. In order to delimit \bfindex{ignored
material} special source comments
@@ -772,7 +771,7 @@
\medskip
- Text may be suppressed in a fine grained manner. We may even drop
+ Text may be suppressed in a fine-grained manner. We may even drop
vital parts of a formal proof, pretending that things have been
simpler than in reality. For example, the following ``fully
automatic'' proof is actually a fake:%
@@ -790,12 +789,12 @@
\end{verbatim}
%(*
- \medskip Ignoring portions of printed does demand some care by the
- writer. First of all, the writer is responsible not to obfuscate
- the underlying formal development in an unduly manner. It is fairly
- easy to invalidate the remaining visible text, e.g.\ by referencing
- questionable formal items (strange definitions, arbitrary axioms
- etc.) that have been hidden from sight beforehand.
+ \medskip Ignoring portions of printed text does demand some care by
+ the writer. First of all, the writer is responsible not to
+ obfuscate the underlying formal development in an unduly manner. It
+ is fairly easy to invalidate the remaining visible text, e.g.\ by
+ referencing questionable formal items (strange definitions,
+ arbitrary axioms etc.) that have been hidden from sight beforehand.
Authentic reports of formal theories, say as part of a library,
usually should refrain from suppressing parts of the text at all.