doc-src/TutorialI/Documents/documents.tex

updated;

\chapter{Presenting theories}
\label{ch:thy-present}

Now that the reader has become sufficiently acquainted with basic formal
theory development in Isabelle/HOL, the subsequent interlude covers the
``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 term language), as well as document
preparation of theory texts using existing PDF-{\LaTeX} technology.

The measure of theory beautification depends on the kind of application one
has in mind, and the intended audience of the final results.  In any case,
users may already benefit themselves from handsome notation available in
interactive development.  Only minimal provisions in theory specifications may
already change the general appearance of formal entities in a significant way.

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: