--- a/doc-src/TutorialI/Documents/documents.tex Tue Jan 08 15:39:35 2002 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex Tue Jan 08 15:39:47 2002 +0100
@@ -2,13 +2,13 @@
\chapter{Presenting theories}
\label{ch:thy-present}
-By virtue of the previous chapters the reader has become sufficiently
+Due to the previous chapters the reader should have become sufficiently
acquainted with basic formal theory development in Isabelle/HOL. The
-subsequent interlude covers the ``marginal'' issue of presenting theories in a
-typographically pleasing manner. Isabelle provides a rich infrastructure for
-concrete syntax (input and output of the $\lambda$-calculus language), as well
-as document preparation of theory texts based on existing PDF-{\LaTeX}
-technology.
+following interlude covers the seemingly ``marginal'' issue of presenting
+theories in a typographically pleasing manner. Isabelle provides a rich
+infrastructure for concrete syntax (input and output of the $\lambda$-calculus
+language), as well as document preparation of theory texts based on existing
+PDF-{\LaTeX} technology.
As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
300 years ago, \emph{notions} are in principle more important than