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