2 \chapter{Presenting theories}
5 Now that the reader has become sufficiently acquainted with basic formal
6 theory development in Isabelle/HOL, the subsequent interlude covers the
7 ``marginal'' issue of presenting theories in a typographically pleasing
8 manner. Isabelle provides a rich infrastructure for concrete syntax (input
9 and output of the $\lambda$-calculus term language), as well as document
10 preparation of theory texts using existing PDF-{\LaTeX} technology.
12 The measure of theory beautification depends on the kind of application one
13 has in mind, and the intended audience of the final results. In any case,
14 users may already benefit themselves from handsome notation available in
15 interactive development. Only minimal provisions in theory specifications may
16 already change the general appearance of formal entities in a significant way.
18 As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
19 300 years ago, \emph{notions} are in principle more important than
20 \emph{notations}, but fair textual representation of ideas is very important
21 to reduce the mental effort in actual applications.
23 \input{Documents/document/Documents.tex}