\chapter{Presenting theories}
\label{ch:thy-present}
Due to the previous chapters the reader should have become sufficiently
acquainted with basic formal 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 (input and output of the $\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 very important
to reduce the mental effort in actual applications.
\input{Documents/document/Documents.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: