--- a/doc-src/TutorialI/Documents/documents.tex Tue Jan 08 17:32:28 2002 +0100
+++ b/doc-src/TutorialI/Documents/documents.tex Tue Jan 08 17:32:40 2002 +0100
@@ -1,19 +1,19 @@
-\chapter{Presenting theories}
+\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. The
-following interlude covers the seemingly ``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.
+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.
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.
+\emph{notations}, but fair textual representation of ideas is vital to reduce
+the mental effort in actual applications.
\input{Documents/document/Documents.tex}