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