
diff -r 5c896eccb290 -r bb6db6c0d4df doc-src/TutorialI/Documents/documents.tex
--- 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}
 




