1 |
1 |
2 \chapter{Presenting theories} |
2 \chapter{Presenting theories} |
3 \label{ch:thy-present} |
3 \label{ch:thy-present} |
4 |
4 |
5 By virtue of the previous chapters the reader has become sufficiently |
5 Due to the previous chapters the reader should have become sufficiently |
6 acquainted with basic formal theory development in Isabelle/HOL. The |
6 acquainted with basic formal theory development in Isabelle/HOL. The |
7 subsequent interlude covers the ``marginal'' issue of presenting theories in a |
7 following interlude covers the seemingly ``marginal'' issue of presenting |
8 typographically pleasing manner. Isabelle provides a rich infrastructure for |
8 theories in a typographically pleasing manner. Isabelle provides a rich |
9 concrete syntax (input and output of the $\lambda$-calculus language), as well |
9 infrastructure for concrete syntax (input and output of the $\lambda$-calculus |
10 as document preparation of theory texts based on existing PDF-{\LaTeX} |
10 language), as well as document preparation of theory texts based on existing |
11 technology. |
11 PDF-{\LaTeX} technology. |
12 |
12 |
13 As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than |
13 As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than |
14 300 years ago, \emph{notions} are in principle more important than |
14 300 years ago, \emph{notions} are in principle more important than |
15 \emph{notations}, but fair textual representation of ideas is very important |
15 \emph{notations}, but fair textual representation of ideas is very important |
16 to reduce the mental effort in actual applications. |
16 to reduce the mental effort in actual applications. |