--- 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