diff -r 83cd2140977d -r 46e3ef8dd9ea doc-src/TutorialI/Documents/documents.tex --- 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}