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