|
11647
|
1 |
|
|
12570
|
2 |
\chapter{Presenting theories}
|
|
|
3 |
\label{ch:thy-present}
|
|
|
4 |
|
|
12666
|
5 |
Due to the previous chapters the reader should have become sufficiently
|
|
12653
|
6 |
acquainted with basic formal theory development in Isabelle/HOL. The
|
|
12666
|
7 |
following interlude covers the seemingly ``marginal'' issue of presenting
|
|
|
8 |
theories in a typographically pleasing manner. Isabelle provides a rich
|
|
|
9 |
infrastructure for concrete syntax (input and output of the $\lambda$-calculus
|
|
|
10 |
language), as well as document preparation of theory texts based on existing
|
|
|
11 |
PDF-{\LaTeX} 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
|
|
|
15 |
\emph{notations}, but fair textual representation of ideas is very important
|
|
|
16 |
to reduce 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:
|