|
11647
|
1 |
|
|
12671
|
2 |
\chapter{Presenting Theories}
|
|
12570
|
3 |
\label{ch:thy-present}
|
|
|
4 |
|
|
12743
|
5 |
By now the reader should have become sufficiently acquainted with elementary
|
|
12764
|
6 |
theory development in Isabelle/HOL\@. The following interlude describes
|
|
|
7 |
how to present theories in a typographically
|
|
12743
|
8 |
pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
|
|
|
9 |
of the underlying $\lambda$-calculus language (see
|
|
12764
|
10 |
{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
|
|
12743
|
11 |
based on existing PDF-{\LaTeX} technology (see
|
|
12764
|
12 |
{\S}\ref{sec:document-preparation}).
|
|
12635
|
13 |
|
|
12743
|
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.
|
|
11647
|
18 |
|
|
48522
|
19 |
\input{document/Documents.tex}
|
|
11647
|
20 |
|
|
|
21 |
%%% Local Variables:
|
|
|
22 |
%%% mode: latex
|
|
|
23 |
%%% TeX-master: t
|
|
|
24 |
%%% End:
|