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}