--- a/doc-src/TutorialI/Documents/documents.tex Mon Jan 14 00:16:43 2002 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex Mon Jan 14 14:39:22 2002 +0100
@@ -2,18 +2,19 @@
\chapter{Presenting Theories}
\label{ch:thy-present}
-Due to the previous chapters the reader should have become sufficiently
-acquainted with elementary theory development in Isabelle/HOL. The following
-interlude covers the seemingly ``marginal'' issue of presenting theories in a
-typographically pleasing manner. Isabelle provides a rich infrastructure for
-concrete syntax of the underlying $\lambda$-calculus language, as well as
-document preparation of theory texts based on existing PDF-{\LaTeX}
-technology.
+By now the reader should have become sufficiently acquainted with elementary
+theory development in Isabelle/HOL. The following interlude covers the
+seemingly ``marginal'' issue of presenting theories in a typographically
+pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
+of the underlying $\lambda$-calculus language (see
+\S\ref{sec:concrete-syntax}), as well as document preparation of theory texts
+based on existing PDF-{\LaTeX} technology (see
+\S\ref{sec:document-preparation}).
-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 vital to reduce
-the mental effort in actual applications.
+As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
+years ago, \emph{notions} are in principle more important than
+\emph{notations}, but suggestive textual representation of ideas is vital to
+reduce the mental effort to comprehend and apply them.
\input{Documents/document/Documents.tex}