doc-src/TutorialI/Documents/documents.tex
changeset 12764 b43333dc6e7d
parent 12743 46e3ef8dd9ea
child 48536 4e2ee88276d2
--- 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