diff -r 2d136f05e164 -r a55c066624eb doc-src/TutorialI/Documents/documents.tex
--- a/doc-src/TutorialI/Documents/documents.tex	Mon Jan 07 18:30:31 2002 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex	Mon Jan 07 18:30:43 2002 +0100
@@ -2,18 +2,13 @@
 \chapter{Presenting theories}
 \label{ch:thy-present}
 
-Now that the reader has 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 term language), as well as document
-preparation of theory texts using existing PDF-{\LaTeX} technology.
-
-The measure of theory beautification depends on the kind of application one
-has in mind, and the intended audience of the final results.  In any case,
-users may already benefit themselves from handsome notation available in
-interactive development.  Only minimal provisions in theory specifications may
-already change the general appearance of formal entities in a significant way.
+By virtue of the previous chapters the reader has 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.
 
 As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
 300 years ago, \emph{notions} are in principle more important than