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