1 |
1 |
2 \chapter{Presenting Theories} |
2 \chapter{Presenting Theories} |
3 \label{ch:thy-present} |
3 \label{ch:thy-present} |
4 |
4 |
5 Due to the previous chapters the reader should have become sufficiently |
5 By now the reader should have become sufficiently acquainted with elementary |
6 acquainted with elementary theory development in Isabelle/HOL. The following |
6 theory development in Isabelle/HOL. The following interlude covers the |
7 interlude covers the seemingly ``marginal'' issue of presenting theories in a |
7 seemingly ``marginal'' issue of presenting theories in a typographically |
8 typographically pleasing manner. Isabelle provides a rich infrastructure for |
8 pleasing manner. Isabelle provides a rich infrastructure for concrete syntax |
9 concrete syntax of the underlying $\lambda$-calculus language, as well as |
9 of the underlying $\lambda$-calculus language (see |
10 document preparation of theory texts based on existing PDF-{\LaTeX} |
10 \S\ref{sec:concrete-syntax}), as well as document preparation of theory texts |
11 technology. |
11 based on existing PDF-{\LaTeX} technology (see |
|
12 \S\ref{sec:document-preparation}). |
12 |
13 |
13 As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than |
14 As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 |
14 300 years ago, \emph{notions} are in principle more important than |
15 years ago, \emph{notions} are in principle more important than |
15 \emph{notations}, but fair textual representation of ideas is vital to reduce |
16 \emph{notations}, but suggestive textual representation of ideas is vital to |
16 the mental effort in actual applications. |
17 reduce the mental effort to comprehend and apply them. |
17 |
18 |
18 \input{Documents/document/Documents.tex} |
19 \input{Documents/document/Documents.tex} |
19 |
20 |
20 %%% Local Variables: |
21 %%% Local Variables: |
21 %%% mode: latex |
22 %%% mode: latex |