|
11647
|
1 |
|
|
12671
|
2 |
\chapter{Presenting Theories}
|
|
12570
|
3 |
\label{ch:thy-present}
|
|
|
4 |
|
|
12666
|
5 |
Due to the previous chapters the reader should have become sufficiently
|
|
12671
|
6 |
acquainted with elementary theory development in Isabelle/HOL. The following
|
|
|
7 |
interlude covers the seemingly ``marginal'' issue of presenting theories in a
|
|
|
8 |
typographically pleasing manner. Isabelle provides a rich infrastructure for
|
|
|
9 |
concrete syntax of the underlying $\lambda$-calculus language, as well as
|
|
|
10 |
document preparation of theory texts based on existing PDF-{\LaTeX}
|
|
|
11 |
technology.
|
|
12635
|
12 |
|
|
|
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
|
|
12671
|
15 |
\emph{notations}, but fair textual representation of ideas is vital to reduce
|
|
|
16 |
the mental effort in actual applications.
|
|
11647
|
17 |
|
|
|
18 |
\input{Documents/document/Documents.tex}
|
|
|
19 |
|
|
|
20 |
%%% Local Variables:
|
|
|
21 |
%%% mode: latex
|
|
|
22 |
%%% TeX-master: t
|
|
|
23 |
%%% End:
|