2 \chapter{Presenting Theories}
5 By now the reader should have become sufficiently acquainted with elementary
6 theory development in Isabelle/HOL\@. The following interlude describes
7 how to present theories in a typographically
8 pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
9 of the underlying $\lambda$-calculus language (see
10 {\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
11 based on existing PDF-{\LaTeX} technology (see
12 {\S}\ref{sec:document-preparation}).
14 As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
15 years ago, \emph{notions} are in principle more important than
16 \emph{notations}, but suggestive textual representation of ideas is vital to
17 reduce the mental effort to comprehend and apply them.
19 \input{document/Documents.tex}