\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, so that we
may now set out on a small interlude concerning the ``marginal'' issue of
presenting theories in a typographically pleasing manner. Isabelle provides a
rich infrastructure for concrete syntax (for input and output of the logical
term language of $\lambda$-calculus), as well as document preparation of
collections of theory texts using existing {\LaTeX} infrastructure.
The overall measure of theory beautification depends on the kind of
application one has in mind, as well as the intended audience of the final
results. In any case, users may already benefit themselves from handsome
notation available in interactive development, while requiring only minimal
provisions as part of the theory specifications.
\input{Documents/document/Documents.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: