diff -r 6cecd9dfd53f -r b43333dc6e7d doc-src/TutorialI/Documents/documents.tex --- a/doc-src/TutorialI/Documents/documents.tex Tue Jan 15 10:24:20 2002 +0100 +++ b/doc-src/TutorialI/Documents/documents.tex Tue Jan 15 13:14:39 2002 +0100 @@ -3,13 +3,13 @@ \label{ch:thy-present} 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 +theory development in Isabelle/HOL\@. The following interlude describes +how to present 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 +{\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}). +{\S}\ref{sec:document-preparation}). As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 years ago, \emph{notions} are in principle more important than