diff -r 3baa6143a9c4 -r e2d44df29c94 doc-src/TutorialI/Documents/documents.tex
--- a/doc-src/TutorialI/Documents/documents.tex	Sat Jan 05 01:14:46 2002 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex	Sat Jan 05 01:15:12 2002 +0100
@@ -2,19 +2,23 @@
 \chapter{Presenting theories}
 \label{ch:thy-present}
 
-Due to the previous chapters the reader should have become sufficiently
-acquainted with basic formal theory development in Isabelle/HOL, so that we
-may now set out on a small interlude concerning the ``marginal'' issue of
-presenting theories in a typographically pleasing manner.  Isabelle provides a
-rich infrastructure for concrete syntax (for input and output of the logical
-term language of $\lambda$-calculus), as well as document preparation of
-collections of theory texts using existing {\LaTeX} infrastructure.
+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 overall measure of theory beautification depends on the kind of
-application one has in mind, as well as the intended audience of the final
-results.  In any case, users may already benefit themselves from handsome
-notation available in interactive development, while requiring only minimal
-provisions as part of the theory specifications.
+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.
+
+As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
+300 years ago, \emph{notions} are in principle more important than
+\emph{notations}, but fair textual representation of ideas is very important
+to reduce the mental effort in actual applications.
 
 \input{Documents/document/Documents.tex}