diff -r e290dadee51c -r 3bd2372e9bed doc-src/TutorialI/Documents/documents.tex
--- a/doc-src/TutorialI/Documents/documents.tex	Thu Dec 20 21:13:22 2001 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex	Thu Dec 20 21:13:36 2001 +0100
@@ -1,9 +1,23 @@
 
-\chapter{Document preparation}
+\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.
+
+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.
 
 \input{Documents/document/Documents.tex}
 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: t