
\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.

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.

\input{Documents/document/Documents.tex}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
