doc-src/TutorialI/Documents/Documents.thy

   The Isar proof language \cite{Wenzel-PhD}, which is not covered in
   this book, admits to write formal proof texts that are acceptable
   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
   proofs formally, the theory sources are turned into typesetting
   instructions in a schematic manner.  This enables users to write

 
 text {*
   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}:
 
   \begin{itemize}

   \texttt{session.tex} will contain {\LaTeX} commands to include all
   generated files in topologically sorted order, so
   \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}
 
   With everything put in its proper place, \texttt{isatool make}

   fall back on DVI output by changing \texttt{usedir} options in
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
   \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
   symbols (see also \S\ref{sec:doc-prep-symbols}).
 

 
 text {*
   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:
   in header position (just before \isakeyword{theory}), within the
   theory body, or within a proof.  The header needs to be treated

   \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
   space and do not really contribute to the content.  They mainly
   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
   syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
   where $text$ is delimited by \verb,",\dots\verb,", or

   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text
   "\<forall>\<exists>"}, according to the standard interpretation of these symbol
   (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.
 *}
 
 
 subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
 
 text {*
   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}.
 
   The {\LaTeX} code produced from Isabelle text follows a relatively

   \medskip The \verb,\isabellestyle, macro provides a high-level
   interface to tune the general appearance of individual symbols.  For
   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.
 *}
 
 

 
 \begin{verbatim}
   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
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the

   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   \end{tabular}
 
   \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:
 *}
 

 \begin{verbatim}
   by (auto(*<*)simp add: int_less_le(*>*))
 \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.
   Other users may need the full information for their own derivative
   work.  If a particular formalization appears inadequate for general